1  /-
  2  Copyright (c) 2017 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro
  5  -/
  6  import data.int.basic algebra.associated data.nat.gcd
src         └────────────┘ └────────────────┘ └──────────┘
  7  
  8  /-- The ring of integers adjoined with a square root of `d`.
  9    These have the form `a + b √d` where `a b : ℤ`. The components
 10    are called `re` and `im` by analogy to the negative `d` case,
 11    but of course both parts are real here since `d` is nonnegative. -/
 12  structure zsqrtd (d : ℤ) := mk {} ::
id                         
src                        
typ                        
 13  (re : ℤ)
id         
src        
typ        
 14  (im : ℤ)
id         
src        
typ        
 15  
 16  prefix `ℤ√`:100 := zsqrtd
id                      └────┘
src                     └────┘
typ                     └────┘
doc                     └────┘
 17  
 18  namespace zsqrtd
 19  section
 20    parameters {d : ℤ}
id                     
src                    
typ                    
 21  
 22    instance : decidable_eq ℤ√d :=
id                └──────────┘ └┘
src               └──────────┘ └┘
typ               └──────────┘ └┘
doc                            └┘
 23    by tactic.mk_dec_eq_instance
id        └───────────────────────┘
src       └───────────────────────┘
typ       └───────────────────────┘
par       └───────────────────────┘
st       └────────────────────────┘
 24  
 25    theorem ext : ∀ {z w : ℤ√d}, z = w ↔ z.re = w.re ∧ z.im = w.im
id                           └┘       └─┘  └─┘  └─┘  └─┘
src                           └┘           └─┘   └─┘   └─┘   └─┘
typ                          └┘       └─┘  └─┘  └─┘  └─┘
doc                           └┘
 26    | ⟨x, y⟩ ⟨x', y'⟩ := ⟨λ h, by injection h; split; assumption,
id                                            
src                                  └────────┘   └───┘  └────────┘
typ                                 └────────┘  └───┘  └────────┘
doc                                  └────────┘   └───┘  └────────┘
txt                                  └────────┘   └───┘  └────────┘
par                                  └────────┘   └───┘  └────────┘
pid                                           
st                                  └─────────────────────────────┘
 27                          λ ⟨h₁, h₂⟩, by congr; assumption⟩
id                             
src                                         └───┘  └────────┘
typ                                        └───┘  └────────┘
doc                                                └────────┘
txt                                         └───┘  └────────┘
par                                         └───┘  └────────┘
st                                         └────────────────┘
 28  
 29    /-- Convert an integer to a `ℤ√d` -/
 30    def of_int (n : ℤ) : ℤ√d := ⟨n, 0⟩
id                         └┘     
src                        └┘
typ                        └┘     
doc                         └┘
 31    @[simp] theorem of_int_re (n : ℤ) : (of_int n).re = n := rfl
id                                         └────┘  └┘       └─┘
src                                        └────┘   └┘        └─┘
typ                                        └────┘  └┘       └─┘
doc      └──┘                               └────┘
 32    @[simp] theorem of_int_im (n : ℤ) : (of_int n).im = 0 := rfl
id                                         └────┘  └┘        └─┘
src                                        └────┘   └┘        └─┘
typ                                        └────┘  └┘        └─┘
doc      └──┘                               └────┘
 33  
 34    /-- The zero of the ring -/
 35    def zero : ℤ√d := of_int 0
id                └┘    └────┘
src               └┘     └────┘
typ               └┘    └────┘
doc               └┘     └────┘
 36    instance : has_zero ℤ√d := ⟨zsqrtd.zero⟩
id                └──────┘ └┘     └─────────┘
src               └──────┘ └┘      └─────────┘
typ               └──────┘ └┘     └─────────┘
doc                        └┘      └─────────┘
 37    @[simp] theorem zero_re : (0 : ℤ√d).re = 0 := rfl
id                                    └┘ └┘        └─┘
src                                   └┘  └┘        └─┘
typ                                   └┘ └┘        └─┘
doc      └──┘                         └┘
 38    @[simp] theorem zero_im : (0 : ℤ√d).im = 0 := rfl
id                                    └┘ └┘        └─┘
src                                   └┘  └┘        └─┘
typ                                   └┘ └┘        └─┘
doc      └──┘                         └┘
 39  
 40    instance : inhabited ℤ√d := ⟨0⟩
id                └───────┘ └┘
src               └───────┘ └┘
typ               └───────┘ └┘
doc                         └┘
 41  
 42    /-- The one of the ring -/
 43    def one : ℤ√d := of_int 1
id               └┘    └────┘
src              └┘     └────┘
typ              └┘    └────┘
doc              └┘     └────┘
 44    instance : has_one ℤ√d := ⟨zsqrtd.one⟩
id                └─────┘ └┘     └────────┘
src               └─────┘ └┘      └────────┘
typ               └─────┘ └┘     └────────┘
doc                       └┘      └────────┘
 45    @[simp] theorem one_re : (1 : ℤ√d).re = 1 := rfl
id                                   └┘ └┘        └─┘
src                                  └┘  └┘        └─┘
typ                                  └┘ └┘        └─┘
doc      └──┘                        └┘
 46    @[simp] theorem one_im : (1 : ℤ√d).im = 0 := rfl
id                                   └┘ └┘        └─┘
src                                  └┘  └┘        └─┘
typ                                  └┘ └┘        └─┘
doc      └──┘                        └┘
 47  
 48    /-- The representative of `√d` in the ring -/
 49    def sqrtd : ℤ√d := ⟨0, 1⟩
id                 └┘
src                └┘
typ                └┘
doc                └┘
 50    @[simp] theorem sqrtd_re : (sqrtd : ℤ√d).re = 0 := rfl
id                                 └───┘   └┘ └┘        └─┘
src                                └───┘   └┘  └┘        └─┘
typ                                └───┘   └┘ └┘        └─┘
doc      └──┘                      └───┘   └┘
 51    @[simp] theorem sqrtd_im : (sqrtd : ℤ√d).im = 1 := rfl
id                                 └───┘   └┘ └┘        └─┘
src                                └───┘   └┘  └┘        └─┘
typ                                └───┘   └┘ └┘        └─┘
doc      └──┘                      └───┘   └┘
 52  
 53    /-- Addition of elements of `ℤ√d` -/
 54    def add : ℤ√d → ℤ√d → ℤ√d
id               └┘  └┘   └┘
src              └┘    └┘    └┘
typ              └┘  └┘   └┘
doc              └┘    └┘    └┘
 55    | ⟨x, y⟩ ⟨x', y'⟩ := ⟨x + x', y + y'⟩
id             └┘  └┘               
src                                   
typ            └┘  └┘               
 56    instance : has_add ℤ√d := ⟨zsqrtd.add⟩
id                └─────┘ └┘     └────────┘
src               └─────┘ └┘      └────────┘
typ               └─────┘ └┘     └────────┘
doc                       └┘      └────────┘
 57    @[simp] theorem add_def (x y x' y' : ℤ) :
id                                          
src                                         
typ                                         
doc      └──┘
 58      (⟨x, y⟩ + ⟨x', y'⟩ : ℤ√d) = ⟨x + x', y + y'⟩ := rfl
id               └┘  └┘    └┘      └┘    └┘     └─┘
src                          └┘                      └─┘
typ              └┘  └┘    └┘      └┘    └┘     └─┘
doc                           └┘
 59    @[simp] theorem add_re : ∀ z w : ℤ√d, (z + w).re = z.re + w.re
id                                     └┘      └┘   └─┘  └─┘
src                                     └┘         └┘    └─┘   └─┘
typ                                    └┘      └┘   └─┘  └─┘
doc      └──┘                           └┘
 60    | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
 61    @[simp] theorem add_im : ∀ z w : ℤ√d, (z + w).im = z.im + w.im
id                                     └┘      └┘   └─┘  └─┘
src                                     └┘         └┘    └─┘   └─┘
typ                                    └┘      └┘   └─┘  └─┘
doc      └──┘                           └┘
 62    | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
 63  
 64    @[simp] theorem bit0_re (z) : (bit0 z : ℤ√d).re = bit0 z.re := add_re _ _
id                                    └──┘    └┘ └┘   └──┘ └─┘    └────┘
src                                   └──┘     └┘  └┘   └──┘  └─┘    └────┘
typ                                   └──┘    └┘ └┘   └──┘ └─┘    └────┘
doc      └──┘                                  └┘
 65    @[simp] theorem bit0_im (z) : (bit0 z : ℤ√d).im = bit0 z.im := add_im _ _
id                                    └──┘    └┘ └┘   └──┘ └─┘    └────┘
src                                   └──┘     └┘  └┘   └──┘  └─┘    └────┘
typ                                   └──┘    └┘ └┘   └──┘ └─┘    └────┘
doc      └──┘                                  └┘
 66  
 67    @[simp] theorem bit1_re (z) : (bit1 z : ℤ√d).re = bit1 z.re := by simp [bit1]
id                                    └──┘    └┘ └┘   └──┘ └─┘             └──┘
src                                   └──┘     └┘  └┘   └──┘  └─┘       └────┘└──┘└─
typ                                   └──┘    └┘ └┘   └──┘ └─┘       └────┘└──┘└─
doc      └──┘                                  └┘                        └────┘    └─
txt                                                                      └────┘    └─
par                                                                      └────┘    └─
pid                                                                              
st                                                                      └────────────
 68    @[simp] theorem bit1_im (z) : (bit1 z : ℤ√d).im = bit0 z.im := by simp [bit1]
id                                    └──┘    └┘ └┘   └──┘ └─┘             └──┘
src  ─┘                               └──┘     └┘  └┘   └──┘  └─┘       └────┘└──┘└─
typ  ─┘                               └──┘    └┘ └┘   └──┘ └─┘       └────┘└──┘└─
doc  ─┘  └──┘                                  └┘                        └────┘    └─
txt  ─┘                                                                  └────┘    └─
par  ─┘                                                                  └────┘    └─
pid  ─┘                                                                          
st   ─┘                                                                 └────────────
 69  
src  
typ  
doc  
txt  
par  
pid  
st   
 70    /-- Negation in `ℤ√d` -/
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 71    def neg : ℤ√d → ℤ√d
id               └┘  └┘
src              └┘    └┘
typ              └┘  └┘
doc              └┘    └┘
 72    | ⟨x, y⟩ := ⟨-x, -y⟩
id                   
src                    
typ                  
 73    instance : has_neg ℤ√d := ⟨zsqrtd.neg⟩
id                └─────┘ └┘     └────────┘
src               └─────┘ └┘      └────────┘
typ               └─────┘ └┘     └────────┘
doc                       └┘      └────────┘
 74    @[simp] theorem neg_re : ∀ z : ℤ√d, (-z).re = -z.re
id                                   └┘    └┘   └─┘
src                                   └┘      └┘    └─┘
typ                                  └┘    └┘   └─┘
doc      └──┘                         └┘
 75    | ⟨x, y⟩ := rfl
id                 └─┘
src                └─┘
typ                └─┘
 76    @[simp] theorem neg_im : ∀ z : ℤ√d, (-z).im = -z.im
id                                   └┘    └┘   └─┘
src                                   └┘      └┘    └─┘
typ                                  └┘    └┘   └─┘
doc      └──┘                         └┘
 77    | ⟨x, y⟩ := rfl
id                 └─┘
src                └─┘
typ                └─┘
 78  
 79    /-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`. -/
 80    def conj : ℤ√d → ℤ√d
id                └┘  └┘
src               └┘    └┘
typ               └┘  └┘
doc               └┘    └┘
 81    | ⟨x, y⟩ := ⟨x, -y⟩
id                   
src                    
typ                  
 82    @[simp] theorem conj_re : ∀ z : ℤ√d, (conj z).re = z.re
id                                    └┘   └──┘  └┘   └─┘
src                                    └┘    └──┘   └┘    └─┘
typ                                   └┘   └──┘  └┘   └─┘
doc      └──┘                          └┘    └──┘
 83    | ⟨x, y⟩ := rfl
id                 └─┘
src                └─┘
typ                └─┘
 84    @[simp] theorem conj_im : ∀ z : ℤ√d, (conj z).im = -z.im
id                                    └┘   └──┘  └┘   └─┘
src                                    └┘    └──┘   └┘    └─┘
typ                                   └┘   └──┘  └┘   └─┘
doc      └──┘                          └┘    └──┘
 85    | ⟨x, y⟩ := rfl
id                 └─┘
src                └─┘
typ                └─┘
 86  
 87    /-- Multiplication in `ℤ√d` -/
 88    def mul : ℤ√d → ℤ√d → ℤ√d
id               └┘  └┘   └┘
src              └┘    └┘    └┘
typ              └┘  └┘   └┘
doc              └┘    └┘    └┘
 89    | ⟨x, y⟩ ⟨x', y'⟩ := ⟨x * x' + d * y * y', x * y' + y * x'⟩
id             └┘  └┘                               
src                                                    
typ            └┘  └┘                               
 90    instance : has_mul ℤ√d := ⟨zsqrtd.mul⟩
id                └─────┘ └┘     └────────┘
src               └─────┘ └┘      └────────┘
typ               └─────┘ └┘     └────────┘
doc                       └┘      └────────┘
 91    @[simp] theorem mul_re : ∀ z w : ℤ√d, (z * w).re = z.re * w.re + d * z.im * w.im
id                                     └┘      └┘   └─┘  └─┘    └─┘  └─┘
src                                     └┘         └┘    └─┘   └─┘      └─┘   └─┘
typ                                    └┘      └┘   └─┘  └─┘    └─┘  └─┘
doc      └──┘                           └┘
 92    | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
 93    @[simp] theorem mul_im : ∀ z w : ℤ√d, (z * w).im = z.re * w.im + z.im * w.re
id                                     └┘      └┘   └─┘  └─┘  └─┘  └─┘
src                                     └┘         └┘    └─┘   └─┘   └─┘   └─┘
typ                                    └┘      └┘   └─┘  └─┘  └─┘  └─┘
doc      └──┘                           └┘
 94    | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
 95  
 96    instance : comm_ring ℤ√d := by refine
id                └───────┘ └┘
src               └───────┘ └┘        └──────
typ               └───────┘ └┘       └──────
doc                         └┘        └──────
txt                                   └──────
par                                   └──────
pid                                         
st                                   └───────
 97    { add            := (+),
id                         
src  ─┘ └─────────────────┘└───
typ  ─┘ └─────────────────┘└───
doc  ─┘ └─────────────────┘ └───
txt  ─┘ └─────────────────┘ └───
par  ─┘ └─────────────────┘ └───
pid  ─┘ └─────────────────┘ └───
st   ───────────────────────────
 98      zero           := 0,
src  ─────────────────────────
typ  ─────────────────────────
doc  ─────────────────────────
txt  ─────────────────────────
par  ─────────────────────────
pid  ─────────────────────────
st   ─────────────────────────
 99      neg            := has_neg.neg,
id                         └─────────┘
src  ─────────────────────┘└─────────┘└─
typ  ─────────────────────┘└─────────┘└─
doc  ─────────────────────┘           └─
txt  ─────────────────────┘           └─
par  ─────────────────────┘           └─
pid  ─────────────────────┘           └─
st   ───────────────────────────────────
100      mul            := (*),
id                         
src  ─────────────────────┘└───
typ  ─────────────────────┘└───
doc  ─────────────────────┘ └───
txt  ─────────────────────┘ └───
par  ─────────────────────┘ └───
pid  ─────────────────────┘ └───
st   ───────────────────────────
101      one            := 1, ..};
src  ───────────────────────────┘
typ  ───────────────────────────┘
doc  ───────────────────────────┘
txt  ───────────────────────────┘
par  ───────────────────────────┘
pid  ───────────────────────────┘
st   ──────────────────────────────
102    { intros, simp [ext, add_mul, mul_add, mul_comm, mul_left_comm] }
id                     └─┘  └─────┘  └─────┘  └──────┘  └───────────┘
src      └────┘  └────┘└─┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘
typ      └────┘  └────┘└─┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘
doc      └────┘  └────┘   └┘       └┘       └┘        └┘             └┘
txt      └────┘  └────┘   └┘       └┘       └┘        └┘             └┘
par      └────┘  └────┘   └┘       └┘       └┘        └┘             └┘
pid                     └┘       └┘       └┘        └┘             
st   ─┘└──────┘└──────────────────────────────────────────────────────┘└┘
103  
104    instance : add_comm_monoid ℤ√d    := by apply_instance
id                └─────────────┘ └┘
src               └─────────────┘ └┘           └──────────────
typ               └─────────────┘ └┘          └──────────────
doc                               └┘           └──────────────
txt                                            └──────────────
par                                            └──────────────
pid                                                          
st                                            └───────────────
105    instance : add_monoid ℤ√d         := by apply_instance
id                └────────┘ └┘
src  ─┘           └────────┘ └┘                └──────────────
typ  ─┘           └────────┘ └┘               └──────────────
doc  ─┘                      └┘                └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
106    instance : monoid ℤ√d             := by apply_instance
id                └────┘ └┘
src  ─┘           └────┘ └┘                    └──────────────
typ  ─┘           └────┘ └┘                   └──────────────
doc  ─┘                  └┘                    └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
107    instance : comm_monoid ℤ√d        := by apply_instance
id                └─────────┘ └┘
src  ─┘           └─────────┘ └┘               └──────────────
typ  ─┘           └─────────┘ └┘              └──────────────
doc  ─┘                       └┘               └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
108    instance : comm_semigroup ℤ√d     := by apply_instance
id                └────────────┘ └┘
src  ─┘           └────────────┘ └┘            └──────────────
typ  ─┘           └────────────┘ └┘           └──────────────
doc  ─┘                          └┘            └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
109    instance : semigroup ℤ√d          := by apply_instance
id                └───────┘ └┘
src  ─┘           └───────┘ └┘                 └──────────────
typ  ─┘           └───────┘ └┘                └──────────────
doc  ─┘                     └┘                 └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
110    instance : add_comm_semigroup ℤ√d := by apply_instance
id                └────────────────┘ └┘
src  ─┘           └────────────────┘ └┘        └──────────────
typ  ─┘           └────────────────┘ └┘       └──────────────
doc  ─┘                              └┘        └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
111    instance : add_semigroup ℤ√d      := by apply_instance
id                └───────────┘ └┘
src  ─┘           └───────────┘ └┘             └──────────────
typ  ─┘           └───────────┘ └┘            └──────────────
doc  ─┘                         └┘             └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
112    instance : comm_semiring ℤ√d      := by apply_instance
id                └───────────┘ └┘
src  ─┘           └───────────┘ └┘             └──────────────
typ  ─┘           └───────────┘ └┘            └──────────────
doc  ─┘                         └┘             └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
113    instance : semiring ℤ√d           := by apply_instance
id                └──────┘ └┘
src  ─┘           └──────┘ └┘                  └──────────────
typ  ─┘           └──────┘ └┘                 └──────────────
doc  ─┘                    └┘                  └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
114    instance : ring ℤ√d               := by apply_instance
id                └──┘ └┘
src  ─┘           └──┘ └┘                      └──────────────
typ  ─┘           └──┘ └┘                     └──────────────
doc  ─┘                └┘                      └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
115    instance : distrib ℤ√d            := by apply_instance
id                └─────┘ └┘
src  ─┘           └─────┘ └┘                   └──────────────
typ  ─┘           └─────┘ └┘                  └──────────────
doc  ─┘                   └┘                   └──────────────
txt  ─┘                                        └──────────────
par  ─┘                                        └──────────────
pid  ─┘                                                      
st   ─┘                                       └───────────────
116  
src  
typ  
doc  
txt  
par  
pid  
st   
117    instance : zero_ne_one_class ℤ√d :=
id                └───────────────┘ └┘
src  ─┘           └───────────────┘ └┘
typ  ─┘           └───────────────┘ └┘
doc  ─┘                             └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
118    { zero := 0, one := 1, zero_ne_one := dec_trivial }
id                                           └─────────┘
src                                          └─────────┘
typ                                          └─────────┘
doc                                          └─────────┘
119  
120    instance : nonzero_comm_ring ℤ√d :=
id                └───────────────┘ └┘
src               └───────────────┘ └┘
typ               └───────────────┘ └┘
doc               └───────────────┘ └┘
121    { ..zsqrtd.comm_ring, ..zsqrtd.zero_ne_one_class }
id         └──────────────┘    └──────────────────────┘
src        └──────────────┘    └──────────────────────┘
typ        └──────────────┘    └──────────────────────┘
122  
123    @[simp] theorem coe_nat_re (n : ℕ) : (n : ℤ√d).re = n :=
id                                             └┘ └┘   
src                                             └┘  └┘  
typ                                            └┘ └┘   
doc      └──┘                                    └┘
124    by induction n; simp *
id                  
src       └────────┘   └──────
typ       └────────┘  └──────
doc       └────────┘   └──────
txt       └────────┘   └──────
par       └────────┘   └──────
pid                       
st       └────────────────────
125    @[simp] theorem coe_nat_im (n : ℕ) : (n : ℤ√d).im = 0 :=
id                                             └┘ └┘  
src  ─┘                                         └┘  └┘  
typ  ─┘                                        └┘ └┘  
doc  ─┘  └──┘                                    └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
126    by induction n; simp *
id                  
src       └────────┘   └──────
typ       └────────┘  └──────
doc       └────────┘   └──────
txt       └────────┘   └──────
par       └────────┘   └──────
pid                       
st       └────────────────────
127    theorem coe_nat_val (n : ℕ) : (n : ℤ√d) = ⟨n, 0⟩ :=
id                                      └┘    
src  ─┘                                  └┘   
typ  ─┘                                 └┘    
doc  ─┘                                   └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
128    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
129  
src  
typ  
doc  
txt  
par  
pid  
st   
130    @[simp] theorem coe_int_re (n : ℤ) : (n : ℤ√d).re = n :=
id                                             └┘ └┘   
src  ─┘                                         └┘  └┘  
typ  ─┘                                        └┘ └┘   
doc  ─┘  └──┘                                    └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
131    by cases n; simp [*, int.of_nat_eq_coe, int.neg_succ_of_nat_eq]
id                         └───────────────┘  └────────────────────┘
src       └────┘   └───────┘└───────────────┘└┘└────────────────────┘└─
typ       └────┘  └───────┘└───────────────┘└┘└────────────────────┘└─
doc       └────┘   └───────┘                 └┘                      └─
txt       └────┘   └───────┘                 └┘                      └─
par       └────┘   └───────┘                 └┘                      └─
pid                   └──┘                 └┘                      
st       └─────────────────────────────────────────────────────────────
132    @[simp] theorem coe_int_im (n : ℤ) : (n : ℤ√d).im = 0 :=
id                                             └┘ └┘  
src  ─┘                                         └┘  └┘  
typ  ─┘                                        └┘ └┘  
doc  ─┘  └──┘                                    └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
133    by cases n; simp *
id              
src       └────┘   └──────
typ       └────┘  └──────
doc       └────┘   └──────
txt       └────┘   └──────
par       └────┘   └──────
pid                   
st       └────────────────
134    theorem coe_int_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩ :=
id                                      └┘    
src  ─┘                                  └┘   
typ  ─┘                                 └┘    
doc  ─┘                                   └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
135    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
136  
src  
typ  
doc  
txt  
par  
pid  
st   
137    instance : char_zero ℤ√d :=
id                └───────┘ └┘
src  ─┘           └───────┘ └┘
typ  ─┘           └───────┘ └┘
doc  ─┘           └───────┘ └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
138    { cast_injective := λ m n, by simp [ext] }
id                                       └─┘
src                                  └────┘└─┘└┘
typ                                └────┘└─┘└┘
doc                                  └────┘   └┘
txt                                  └────┘   └┘
par                                  └────┘   └┘
pid                                         
st                                  └──────────┘
139  
140    @[simp] theorem of_int_eq_coe (n : ℤ) : (of_int n : ℤ√d) = n :=
id                                             └────┘    └┘   
src                                            └────┘     └┘   
typ                                            └────┘    └┘   
doc      └──┘                                   └────┘     └┘
141    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143    @[simp] theorem smul_val (n x y : ℤ) : (n : ℤ√d) * ⟨x, y⟩ = ⟨n * x, n * y⟩ :=
id                                               └┘                
src  ─┘                                           └┘                     
typ  ─┘                                          └┘                
doc  ─┘  └──┘                                      └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
144    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
145  
src  
typ  
doc  
txt  
par  
pid  
st   
146    @[simp] theorem muld_val (x y : ℤ) : sqrtd * ⟨x, y⟩ = ⟨d * y, x⟩ :=
id                                         └───┘             
src  ─┘                                    └───┘             
typ  ─┘                                    └───┘             
doc  ─┘  └──┘                               └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
147    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149    @[simp] theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n * y, n * x⟩ :=
id                                            └───┘      └┘                  
src  ─┘                                       └───┘       └┘                        
typ  ─┘                                       └───┘      └┘                  
doc  ─┘  └──┘                                  └───┘        └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
150    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
151  
src  
typ  
doc  
txt  
par  
pid  
st   
152    theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd * y :=
id                                          └┘     └───┘  
src  ─┘                                       └┘       └───┘ 
typ  ─┘                                     └┘     └───┘  
doc  ─┘                                        └┘         └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
153    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
154  
src  
typ  
doc  
txt  
par  
pid  
st   
155    theorem mul_conj {x y : ℤ} : (⟨x, y⟩ * conj ⟨x, y⟩ : ℤ√d) = x * x - d * y * y :=
id                                        └──┘        └┘           
src  ─┘                                     └──┘          └┘               
typ  ─┘                                   └──┘        └┘           
doc  ─┘                                       └──┘          └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
156    by simp [ext, mul_comm]
id              └─┘  └──────┘
src       └────┘└─┘└┘└──────┘└─
typ       └────┘└─┘└┘└──────┘└─
doc       └────┘   └┘        └─
txt       └────┘   └┘        └─
par       └────┘   └┘        └─
pid              └┘        
st       └─────────────────────
157  
src  
typ  
doc  
txt  
par  
pid  
st   
158    theorem conj_mul : Π {a b : ℤ√d}, conj (a * b) = conj a * conj b :=
id                                 └┘   └──┘       └──┘   └──┘ 
src  ─┘                            └┘    └──┘         └──┘    └──┘
typ  ─┘                            └┘   └──┘       └──┘   └──┘ 
doc  ─┘                            └┘    └──┘           └──┘     └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
159    by simp [ext]
id              └─┘
src       └────┘└─┘└─
typ       └────┘└─┘└─
doc       └────┘   └─
txt       └────┘   └─
par       └────┘   └─
pid              
st       └───────────
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161    protected lemma coe_int_add (m n : ℤ) : (↑(m + n) : ℤ√d) = ↑m + ↑n := by simp [ext]
id                                                    └┘                  └─┘
src  ─┘                                                 └┘               └────┘└─┘└─
typ  ─┘                                               └┘            └────┘└─┘└─
doc  ─┘                                                    └┘                   └────┘   └─
txt  ─┘                                                                         └────┘   └─
par  ─┘                                                                         └────┘   └─
pid  ─┘                                                                                
st   ─┘                                                                        └───────────
162    protected lemma coe_int_sub (m n : ℤ) : (↑(m - n) : ℤ√d) = ↑m - ↑n := by simp [ext]
id                                                    └┘                  └─┘
src  ─┘                                                 └┘               └────┘└─┘└─
typ  ─┘                                               └┘            └────┘└─┘└─
doc  ─┘                                                    └┘                   └────┘   └─
txt  ─┘                                                                         └────┘   └─
par  ─┘                                                                         └────┘   └─
pid  ─┘                                                                                
st   ─┘                                                                        └───────────
163    protected lemma coe_int_mul (m n : ℤ) : (↑(m * n) : ℤ√d) = ↑m * ↑n := by simp [ext]
id                                                    └┘                  └─┘
src  ─┘                                                 └┘               └────┘└─┘└─
typ  ─┘                                               └┘            └────┘└─┘└─
doc  ─┘                                                    └┘                   └────┘   └─
txt  ─┘                                                                         └────┘   └─
par  ─┘                                                                         └────┘   └─
pid  ─┘                                                                                
st   ─┘                                                                        └───────────
164    protected lemma coe_int_inj {m n : ℤ} (h : (↑m : ℤ√d) = ↑n) : m = n :=
id                                                   └┘         
src  ─┘                                               └┘           
typ  ─┘                                              └┘         
doc  ─┘                                                 └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
165    by simpa using congr_arg re h
id                    └───────┘ └┘ 
src       └──────────┘└───────┘└┘ 
typ       └──────────┘└───────┘└┘
doc       └──────────┘            
txt       └──────────┘            
par       └──────────┘            
pid            └────┘            
st       └───────────────────────────
166  
src  
typ  
doc  
txt  
par  
pid  
st   
167    /-- Read `sq_le a c b d` as `a √c ≤ b √d` -/
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
168    def sq_le (a c b d : ℕ) : Prop := c*a*a ≤ d*b*b
id                                        
src                                            
typ                                       
169  
170    theorem sq_le_of_le {c d x y z w : ℕ} (xz : z ≤ x) (yw : y ≤ w) (xy : sq_le x c y d) : sq_le z c w d :=
id                                                                    └───┘        └───┘    
src                                                                       └───┘            └───┘
typ                                                                   └───┘        └───┘    
doc                                                                          └───┘            └───┘
171    le_trans (mul_le_mul (nat.mul_le_mul_left _ xz) xz (nat.zero_le _) (nat.zero_le _)) $
id     └──────┘  └────────┘  └─────────────────┘   └┘  └┘  └─────────┘     └─────────┘
src    └──────┘  └────────┘  └─────────────────┘           └─────────┘     └─────────┘
typ    └──────┘  └────────┘  └─────────────────┘   └┘  └┘  └─────────┘     └─────────┘
172      le_trans xy (mul_le_mul (nat.mul_le_mul_left _ yw) yw (nat.zero_le _) (nat.zero_le _))
id       └──────┘ └┘  └────────┘  └─────────────────┘   └┘  └┘  └─────────┘     └─────────┘
src      └──────┘     └────────┘  └─────────────────┘           └─────────┘     └─────────┘
typ      └──────┘ └┘  └────────┘  └─────────────────┘   └┘  └┘  └─────────┘     └─────────┘
173  
174    theorem sq_le_add_mixed {c d x y z w : ℕ} (xy : sq_le x c y d) (zw : sq_le z c w d) :
id                                                    └───┘            └───┘    
src                                                   └───┘                └───┘
typ                                                   └───┘            └───┘    
doc                                                    └───┘                └───┘
175      c * (x * z) ≤ d * (y * w) :=
id                    
src                       
typ                   
176    nat.mul_self_le_mul_self_iff.2 $
id     └──────────────────────────┘
src    └──────────────────────────┘
typ    └──────────────────────────┘
177    by simpa [mul_comm, mul_left_comm] using
id               └──────┘  └───────────┘
src       └─────┘└──────┘└┘└───────────┘└───────
typ       └─────┘└──────┘└┘└───────────┘└───────
doc       └─────┘        └┘             └───────
txt       └─────┘        └┘             └───────
par       └─────┘        └┘             └───────
pid                    └┘             └─────
st       └──────────────────────────────────────
178       mul_le_mul xy zw (nat.zero_le _) (nat.zero_le _)
id        └────────┘ └┘ └┘                  └─────────┘
src  ────┘└────────┘                └──┘ └─────────┘└───
typ  ────┘└────────┘└┘└┘            └──┘ └─────────┘└───
doc  ────┘                          └──┘            └───
txt  ────┘                          └──┘            └───
par  ────┘                          └──┘            └───
pid  ────┘                          └──┘            └─┘
st   ──────────────────────────────────────────────────────
179  
src  
typ  
doc  
txt  
par  
pid  
st   
180    theorem sq_le_add {c d x y z w : ℕ} (xy : sq_le x c y d) (zw : sq_le z c w d) :
id                                              └───┘            └───┘    
src  ─┘                                         └───┘                └───┘
typ  ─┘                                         └───┘            └───┘    
doc  ─┘                                          └───┘                └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
181      sq_le (x + z) c (y + w) d :=
id       └───┘            
src      └───┘             
typ      └───┘            
doc      └───┘
182    begin
st     └─────
183      have xz := sq_le_add_mixed xy zw,
id                  └─────────────┘ └┘ └┘
src      └─────────┘└─────────────┘  
typ      └─────────┘└─────────────┘└┘└┘
doc      └─────────┘                 
txt      └─────────┘                 
par      └─────────┘                 
pid      └─────┘└─┘                 
st   ───────────────────────────────────┘└─
184      simp [sq_le, mul_assoc] at xy zw,
id             └───┘  └───────┘
src      └────┘└───┘└┘└───────┘└────────┘
typ      └────┘└───┘└┘└───────┘└────────┘
doc      └────┘└───┘└┘         └────────┘
txt      └────┘     └┘         └────────┘
par      └────┘     └┘         └────────┘
pid               └┘         └──────┘
st   ───────────────────────────────────┘└─
185      simp [sq_le, mul_add, mul_comm, mul_left_comm, add_le_add, *]
id             └───┘  └─────┘  └──────┘  └───────────┘  └────────┘
src      └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└────────┘└────
typ      └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└────────┘└────
doc      └────┘└───┘└┘       └┘        └┘             └┘          └────
txt      └────┘     └┘       └┘        └┘             └┘          └────
par      └────┘     └┘       └┘        └┘             └┘          └────
pid               └┘       └┘        └┘             └┘          └──┘
st   ──────────────────────────────────────────────────────────────────
186    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
187  
188    theorem sq_le_cancel {c d x y z w : ℕ} (zw : sq_le y d x c) (h : sq_le (x + z) c (y + w) d) : sq_le z c w d :=
id                                                 └───┘           └───┘                └───┘    
src                                                └───┘               └───┘                      └───┘
typ                                                └───┘           └───┘                └───┘    
doc                                                 └───┘               └───┘                        └───┘
189    begin
st     └─────
190      apply le_of_not_gt,
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────┘└─
191      intro l,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
192      refine not_le_of_gt _ h,
id              └──────────┘   
src      └─────┘└──────────┘└─┘
typ      └─────┘└──────────┘└─┘
doc      └─────┘            └─┘
txt      └─────┘            └─┘
par      └─────┘            └─┘
pid                        └─┘
st   ──────────────────────────┘└─
193      simp [sq_le, mul_add, mul_comm, mul_left_comm],
id             └───┘  └─────┘  └──────┘  └───────────┘
src      └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘
typ      └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘
doc      └────┘└───┘└┘       └┘        └┘             
txt      └────┘     └┘       └┘        └┘             
par      └────┘     └┘       └┘        └┘             
pid               └┘       └┘        └┘             
st   ─────────────────────────────────────────────────┘└─
194      have hm := sq_le_add_mixed zw (le_of_lt l),
id                  └─────────────┘ └┘  └──────┘ 
src      └─────────┘└─────────────┘   └──────┘ 
typ      └─────────┘└─────────────┘└┘ └──────┘
doc      └─────────┘                           
txt      └─────────┘                           
par      └─────────┘                           
pid      └─────┘└─┘                           
st   ─────────────────────────────────────────────┘└─
195      simp [sq_le, mul_assoc] at l zw,
id             └───┘  └───────┘
src      └────┘└───┘└┘└───────┘└───────┘
typ      └────┘└───┘└┘└───────┘└───────┘
doc      └────┘└───┘└┘         └───────┘
txt      └────┘     └┘         └───────┘
par      └────┘     └┘         └───────┘
pid               └┘         └─────┘
st   ──────────────────────────────────┘└─
196      exact lt_of_le_of_lt (add_le_add_right zw _)
id             └────────────┘  └──────────────┘ └┘
src      └────┘└────────────┘ └──────────────┘  └───
typ      └────┘└────────────┘ └──────────────┘└┘└───
doc      └────┘                                 └───
txt      └────┘                                 └───
par      └────┘                                 └───
pid                                            └───
st   ─────────────────────────────────────────────────
197        (add_lt_add_left (add_lt_add_of_le_of_lt hm (add_lt_add_of_le_of_lt hm l)) _)
id          └─────────────┘                             └────────────────────┘ └┘ 
src  ─────┘ └─────────────┘                          └────────────────────┘   └─────
typ  ─────┘ └─────────────┘                          └────────────────────┘└┘└─────
doc  ─────┘                                                                   └─────
txt  ─────┘                                                                   └─────
par  ─────┘                                                                   └─────
pid  ─────┘                                                                   └───┘
st   ────────────────────────────────────────────────────────────────────────────────────
198    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
199  
200    theorem sq_le_smul {c d x y : ℕ} (n : ℕ) (xy : sq_le x c y d) : sq_le (n * x) c (n * y) d :=
id                                                  └───┘        └───┘            
src                                                 └───┘            └───┘             
typ                                                 └───┘        └───┘            
doc                                                   └───┘            └───┘
201    by simpa [sq_le, mul_left_comm, mul_assoc] using
id               └───┘  └───────────┘  └───────┘
src       └─────┘└───┘└┘└───────────┘└┘└───────┘└───────
typ       └─────┘└───┘└┘└───────────┘└┘└───────┘└───────
doc       └─────┘└───┘└┘             └┘         └───────
txt       └─────┘     └┘             └┘         └───────
par       └─────┘     └┘             └┘         └───────
pid                 └┘             └┘         └─────
st       └──────────────────────────────────────────────
202       nat.mul_le_mul_left (n * n) xy
id        └─────────────────┘       └┘
src  ────┘└─────────────────┘   └┘  
typ  ────┘└─────────────────┘  └┘└┘
doc  ────┘                       └┘  
txt  ────┘                       └┘  
par  ────┘                       └┘  
pid  ────┘                       └┘  
st   ────────────────────────────────────
203  
src  
typ  
doc  
txt  
par  
pid  
st   
204    theorem sq_le_mul {d x y z w : ℕ} :
id                                    
src  ─┘                               
typ  ─┘                               
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
205      (sq_le x 1 y d → sq_le z 1 w d → sq_le (x * w + y * z) d (x * z + d * y * w) 1) ∧
id        └───┘        └───┘        └───┘                         
src       └───┘           └───┘           └───┘                                   
typ       └───┘        └───┘        └───┘                         
doc       └───┘           └───┘           └───┘
206      (sq_le x 1 y d → sq_le w d z 1 → sq_le (x * z + d * y * w) 1 (x * w + y * z) d) ∧
id        └───┘        └───┘        └───┘                         
src       └───┘           └───┘           └───┘                                   
typ       └───┘        └───┘        └───┘                         
doc       └───┘           └───┘           └───┘
207      (sq_le y d x 1 → sq_le z 1 w d → sq_le (x * z + d * y * w) 1 (x * w + y * z) d) ∧
id        └───┘        └───┘        └───┘                         
src       └───┘           └───┘           └───┘                                   
typ       └───┘        └───┘        └───┘                         
doc       └───┘           └───┘           └───┘
208      (sq_le y d x 1 → sq_le w d z 1 → sq_le (x * w + y * z) d (x * z + d * y * w) 1) :=
id        └───┘        └───┘        └───┘                    
src       └───┘           └───┘           └───┘                            
typ       └───┘        └───┘        └───┘                    
doc       └───┘           └───┘           └───┘
209    by refine ⟨_, _, _, _⟩; {
src       └─────┘ └─────────┘
typ       └─────┘ └─────────┘
doc       └─────┘ └─────────┘
txt       └─────┘ └─────────┘
par       └─────┘ └─────────┘
pid              └─────────┘
st       └────────────────────┘└─
210      intros xy zw,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid            └────┘
st   ───────────────┘└─
211      have := int.mul_nonneg (sub_nonneg_of_le (int.coe_nat_le_coe_nat_of_le xy))
id               └────────────┘                                                 └┘
src      └──────┘└────────────┘                                                └──
typ      └──────┘└────────────┘                                              └┘└──
doc      └──────┘                                                              └──
txt      └──────┘                                                              └──
par      └──────┘                                                              └──
pid      └───┘└─┘                                                              └──
st   ────────────────────────────────────────────────────────────────────────────────
212                             (sub_nonneg_of_le (int.coe_nat_le_coe_nat_of_le zw)),
id                               └──────────────┘  └──────────────────────────┘ └┘
src  ──────────────────────────┘ └──────────────┘ └──────────────────────────┘  └┘
typ  ──────────────────────────┘ └──────────────┘ └──────────────────────────┘└┘└┘
doc  ──────────────────────────┘                                                └┘
txt  ──────────────────────────┘                                                └┘
par  ──────────────────────────┘                                                └┘
pid  ──────────────────────────┘                                                └┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
213      refine int.le_of_coe_nat_le_coe_nat (le_of_sub_nonneg _),
id              └──────────────────────────┘  └──────────────┘
src      └─────┘└──────────────────────────┘ └──────────────┘└─┘
typ      └─────┘└──────────────────────────┘ └──────────────┘└─┘
doc      └─────┘                                             └─┘
txt      └─────┘                                             └─┘
par      └─────┘                                             └─┘
pid                                                         └─┘
st   ───────────────────────────────────────────────────────────┘└─
214      simpa [mul_add, mul_left_comm, mul_comm] }
id              └─────┘  └───────────┘  └──────┘
src      └─────┘└─────┘└┘└───────────┘└┘└──────┘└┘
typ      └─────┘└─────┘└┘└───────────┘└┘└──────┘└┘
doc      └─────┘       └┘             └┘        └┘
txt      └─────┘       └┘             └┘        └┘
par      └─────┘       └┘             └┘        └┘
pid                  └┘             └┘        
st   ────────────────────────────────────────────┘└┘
215  
216    /-- "Generalized" `nonneg`. `nonnegg c d x y` means `a √c + b √d ≥ 0`;
217      we are interested in the case `c = 1` but this is more symmetric -/
218    def nonnegg (c d : ℕ) : ℤ → ℤ → Prop
id                              
src                              
typ                             
219    | (a : ℕ) (b : ℕ) := true
id                        └──┘
src                       └──┘
typ                       └──┘
220    | (a : ℕ) -[1+ b] := sq_le (b+1) c a d
id             └──┘     └───┘         
src             └──┘      └───┘   
typ            └──┘     └───┘         
doc                         └───┘
221    | -[1+ a] (b : ℕ) := sq_le (a+1) d b c
id       └──┘           └───┘         
src      └──┘             └───┘   
typ      └──┘           └───┘         
doc                         └───┘
222    | -[1+ a] -[1+ b] := false
id       └──┘   └──┘      └───┘
src      └──┘   └──┘      └───┘
typ      └──┘   └──┘      └───┘
223  
224    theorem nonnegg_comm {c d : ℕ} {x y : ℤ} : nonnegg c d x y = nonnegg d c y x :=
id                                              └─────┘      └─────┘    
src                                             └─────┘          └─────┘
typ                                             └─────┘      └─────┘    
doc                                               └─────┘           └─────┘
225    by induction x; induction y; refl
id                              
src       └────────┘   └────────┘   └────
typ       └────────┘  └────────┘  └────
doc       └────────┘   └────────┘   └────
txt       └────────┘   └────────┘   └────
par       └────────┘   └────────┘   └────
pid                                   
st       └───────────────────────────────
226  
src  
typ  
doc  
txt  
par  
pid  
st   
227    theorem nonnegg_neg_pos {c d} : Π {a b : ℕ}, nonnegg c d (-a) b ↔ sq_le a d b c
id                                                └─────┘        └───┘    
src  ─┘                                            └─────┘            └───┘
typ  ─┘                                           └─────┘        └───┘    
doc  ─┘                                             └─────┘              └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
228    | 0     b := ⟨by simp [sq_le, nat.zero_le], λa, trivial⟩
id                            └───┘  └─────────┘      └─────┘
src                     └────┘└───┘└┘└─────────┘      └─────┘
typ                     └────┘└───┘└┘└─────────┘     └─────┘
doc                     └────┘└───┘└┘           
txt                     └────┘     └┘           
par                     └────┘     └┘           
pid                              └┘           
st                     └────────────────────────┘
229    | (a+1) b := by rw ← int.neg_succ_of_nat_coe; refl
id                         └─────────────────────┘
src                   └───┘└─────────────────────┘  └────
typ                   └───┘└─────────────────────┘  └────
doc                    └───┘                         └────
txt                    └───┘                         └────
par                    └───┘                         └────
pid                      └─┘                             
st                    └───────────────────────────────────
230  
src  
typ  
doc  
txt  
par  
pid  
st   
231    theorem nonnegg_pos_neg {c d} {a b : ℕ} : nonnegg c d a (-b) ↔ sq_le b c a d :=
id                                              └─────┘        └───┘    
src  ─┘                                         └─────┘            └───┘
typ  ─┘                                         └─────┘        └───┘    
doc  ─┘                                          └─────┘              └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
232    by rw nonnegg_comm; exact nonnegg_neg_pos
id           └──────────┘        └─────────────┘
src       └─┘└──────────┘  └────┘└─────────────┘
typ       └─┘└──────────┘  └────┘└─────────────┘
doc       └─┘              └────┘               
txt       └─┘              └────┘               
par       └─┘              └────┘               
pid                                           
st       └───────────────────────────────────────
233  
src  
typ  
doc  
txt  
par  
pid  
st   
234    theorem nonnegg_cases_right {c d} {a : ℕ} : Π {b : ℤ}, (Π x : ℕ, b = -x → sq_le x c a d) → nonnegg c d a b
id                                                                      └───┘        └─────┘    
src  ─┘                                                                     └───┘            └─────┘
typ  ─┘                                                                 └───┘        └─────┘    
doc  ─┘                                                                          └───┘            └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
235    | (b:nat) h := trivial
id          └─┘       └─────┘
src         └─┘       └─────┘
typ         └─┘       └─────┘
236    | -[1+ b] h := h (b+1) rfl
id       └──┘             └─┘
src      └──┘               └─┘
typ      └──┘             └─┘
237  
238    theorem nonnegg_cases_left {c d} {b : ℕ} {a : ℤ} (h : Π x : ℕ, a = -x → sq_le x d b c) : nonnegg c d a b :=
id                                                                      └───┘        └─────┘    
src                                                                       └───┘            └─────┘
typ                                                                     └───┘        └─────┘    
doc                                                                            └───┘            └─────┘
239    cast nonnegg_comm (nonnegg_cases_right h)
id     └──┘ └──────────┘  └─────────────────┘ 
src    └──┘ └──────────┘  └─────────────────┘
typ    └──┘ └──────────┘  └─────────────────┘ 
240  
241  section norm
242  
243  def norm (n : ℤ√d) : ℤ := n.re * n.re - d * n.im * n.im
id                 └┘        └─┘  └─┘    └─┘  └─┘
src                └┘          └─┘   └─┘      └─┘   └─┘
typ                └┘        └─┘  └─┘    └─┘  └─┘
doc                └┘
244  
245  @[simp] lemma norm_zero : norm 0 = 0 := by simp [norm]
id                             └──┘                  └──┘
src                            └──┘            └────┘└──┘└─
typ                            └──┘            └────┘└──┘└─
doc    └──┘                                     └────┘    └─
txt                                             └────┘    └─
par                                             └────┘    └─
pid                                                     
st                                             └────────────
246  
src  
typ  
doc  
txt  
par  
pid  
st   
247  @[simp] lemma norm_one : norm 1 = 1 := by simp [norm]
id                            └──┘                  └──┘
src                           └──┘            └────┘└──┘└─
typ                           └──┘            └────┘└──┘└─
doc    └──┘                                    └────┘    └─
txt                                            └────┘    └─
par                                            └────┘    └─
pid                                                    
st                                            └────────────
248  
src  
typ  
doc  
txt  
par  
pid  
st   
249  @[simp] lemma norm_int_cast (n : ℤ) : norm n = n * n := by simp [norm]
id                                        └──┘                  └──┘
src                                       └──┘               └────┘└──┘└─
typ                                       └──┘            └────┘└──┘└─
doc    └──┘                                                     └────┘    └─
txt                                                             └────┘    └─
par                                                             └────┘    └─
pid                                                                     
st                                                             └────────────
250  
src  
typ  
doc  
txt  
par  
pid  
st   
251  @[simp] lemma norm_nat_cast (n : ℕ) : norm n = n * n := norm_int_cast n
id                                        └──┘         └───────────┘ 
src                                       └──┘            └───────────┘
typ                                       └──┘         └───────────┘ 
doc    └──┘
252  
253  @[simp] lemma norm_mul (n m : ℤ√d) : norm (n * m) = norm n * norm m :=
id                                 └┘    └──┘       └──┘   └──┘ 
src                                └┘     └──┘         └──┘    └──┘
typ                                └┘    └──┘       └──┘   └──┘ 
doc    └──┘                        └┘
254  by simp [norm, mul_add, add_mul, mul_comm, mul_assoc, mul_left_comm]
id            └──┘  └─────┘  └─────┘  └──────┘  └───────┘  └───────────┘
src     └────┘└──┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ     └────┘└──┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc     └────┘    └┘       └┘       └┘        └┘         └┘             └─
txt     └────┘    └┘       └┘       └┘        └┘         └┘             └─
par     └────┘    └┘       └┘       └┘        └┘         └┘             └─
pid             └┘       └┘       └┘        └┘         └┘             
st     └──────────────────────────────────────────────────────────────────
255  
src  
typ  
doc  
txt  
par  
pid  
st   
256  lemma norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * n.conj :=
id                               └┘     └──┘    └┘     └───┘
src                              └┘      └──┘     └┘        └───┘
typ                              └┘     └──┘    └┘     └───┘
doc                              └┘               └┘          └───┘
257  by cases n; simp [norm, conj, zsqrtd.ext, mul_comm]
id                    └──┘  └──┘  └────────┘  └──────┘
src     └────┘   └────┘└──┘└┘└──┘└┘└────────┘└┘└──────┘└─
typ     └────┘  └────┘└──┘└┘└──┘└┘└────────┘└┘└──────┘└─
doc     └────┘   └────┘    └┘└──┘└┘          └┘        └─
txt     └────┘   └────┘    └┘    └┘          └┘        └─
par     └────┘   └────┘    └┘    └┘          └┘        └─
pid                     └┘    └┘          └┘        
st     └─────────────────────────────────────────────────
258  
src  
typ  
doc  
txt  
par  
pid  
st   
259  instance : is_monoid_hom norm :=
id              └───────────┘ └──┘
src             └───────────┘ └──┘
typ             └───────────┘ └──┘
doc             └───────────┘
260  { map_one := norm_one, map_mul := norm_mul }
id                └──────┘             └──────┘
src               └──────┘             └──────┘
typ               └──────┘             └──────┘
261  
262  lemma norm_nonneg (hd : d ≤ 0) (n : ℤ√d) : 0 ≤ n.norm :=
id                                     └┘       └───┘
src                                     └┘         └───┘
typ                                    └┘       └───┘
doc                                      └┘
263  add_nonneg (mul_self_nonneg _)
id   └────────┘  └─────────────┘
src  └────────┘  └─────────────┘
typ  └────────┘  └─────────────┘
264    (by rw [mul_assoc, neg_mul_eq_neg_mul];
id             └───────┘  └────────────────┘
src        └──┘└───────┘└┘└────────────────┘
typ        └──┘└───────┘└┘└────────────────┘
doc        └──┘         └┘                  
txt        └──┘         └┘                  
par        └──┘         └┘                  
pid          └┘         └┘                  
st        └────────────┘└──────────────────┘└─
265      exact (mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)))
id              └────────┘  └────────┘   └┘   └─────────────┘
src      └────┘ └────────┘ └────────┘└─┘  └┘ └─────────────┘└──┘
typ      └────┘ └────────┘ └────────┘└─┘└┘└┘ └─────────────┘└──┘
doc      └────┘                      └─┘  └┘                └──┘
txt      └────┘                      └─┘  └┘                └──┘
par      └────┘                      └─┘  └┘                └──┘
pid                                 └─┘  └┘                └──┘
st   ───────────────────────────────────────────────────────────┘
266  
267  lemma norm_eq_one_iff {x : ℤ√d} : x.norm.nat_abs = 1 ↔ is_unit x :=
id                              └┘    └───┘└──────┘     └─────┘ 
src                             └┘      └───┘└──────┘     └─────┘
typ                             └┘    └───┘└──────┘     └─────┘ 
doc                             └┘                          └─────┘
268  ⟨λ h, is_unit_iff_dvd_one.2 $
id        └─────────────────┘
src        └─────────────────┘
typ       └─────────────────┘
269    (le_total 0 (norm x)).cases_on
id      └──────┘    └──┘   └──────┘
src     └──────┘    └──┘    └──────┘
typ     └──────┘    └──┘   └──────┘
270      (λ hx, show x ∣ 1, from ⟨x.conj,
id          └┘                  └───┘
src                               └───┘
typ         └┘                  └───┘
doc                                └───┘
271        by rwa [← int.coe_nat_inj', int.nat_abs_of_nonneg hx,
id                   └──────────────┘  └───────────────────┘ └┘
src           └─────┘└──────────────┘└┘└───────────────────┘  └─
typ           └─────┘└──────────────┘└┘└───────────────────┘└┘└─
doc           └─────┘                └┘                       └─
txt           └─────┘                └┘                       └─
par           └─────┘                └┘                       └─
pid              └──┘                └┘                       └─
st           └──────────────────────┘└────────────────────────┘└─
272          ← @int.cast_inj (ℤ√d) _ _, norm_eq_mul_conj, eq_comm] at h⟩)
id              └──────────┘           └──────────────┘  └─────┘
src  ─────────┘ └──────────┘    └─────┘└──────────────┘└┘└─────┘└────┘
typ  ─────────┘ └──────────┘   └─────┘└──────────────┘└┘└─────┘└────┘
doc  ─────────┘                 └─────┘                └┘       └────┘
txt  ─────────┘                 └─────┘                └┘       └────┘
par  ─────────┘                 └─────┘                └┘       └────┘
pid  ─────────┘                 └─────┘                └┘       └───┘
st   ────────────────────────────────┘└────────────────┘└───────┘└───┘
273      (λ hx, show x ∣ 1, from ⟨- x.conj,
id          └┘                   └───┘
src                                └───┘
typ         └┘                   └───┘
doc                                  └───┘
274        by rwa [← int.coe_nat_inj', int.of_nat_nat_abs_of_nonpos hx,
id                   └──────────────┘  └──────────────────────────┘ └┘
src           └─────┘└──────────────┘└┘└──────────────────────────┘  └─
typ           └─────┘└──────────────┘└┘└──────────────────────────┘└┘└─
doc           └─────┘                └┘                              └─
txt           └─────┘                └┘                              └─
par           └─────┘                └┘                              └─
pid              └──┘                └┘                              └─
st           └──────────────────────┘└───────────────────────────────┘└─
275          ← @int.cast_inj (ℤ√d) _ _, int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg,
id              └──────────┘           └──────────┘  └──────────────┘  └────────────────┘
src  ─────────┘ └──────────┘    └─────┘└──────────┘└┘└──────────────┘└┘└────────────────┘└─
typ  ─────────┘ └──────────┘   └─────┘└──────────┘└┘└──────────────┘└┘└────────────────┘└─
doc  ─────────┘                 └─────┘            └┘                └┘                  └─
txt  ─────────┘                 └─────┘            └┘                └┘                  └─
par  ─────────┘                 └─────┘            └┘                └┘                  └─
pid  ─────────┘                 └─────┘            └┘                └┘                  └─
st   ────────────────────────────────┘└────────────┘└────────────────┘└──────────────────┘└─
276          eq_comm] at h⟩),
id           └─────┘
src  ───────┘└─────┘└────┘
typ  ───────┘└─────┘└────┘
doc  ───────┘       └────┘
txt  ───────┘       └────┘
par  ───────┘       └────┘
pid  ───────┘       └───┘
st   ──────────────┘└───┘
277  λ h, let ⟨y, hy⟩ := is_unit_iff_dvd_one.1 h in begin
id       └─┘            └─────────────────┘  
src                      └─────────────────┘
typ      └─┘            └─────────────────┘  
st                                                  └─────
278    have := congr_arg (int.nat_abs ∘ norm) hy,
id             └───────┘  └─────────┘  └──┘  └┘
src    └──────┘└───────┘ └─────────┘└──┘└┘
typ    └──────┘└───────┘ └─────────┘└──┘└┘└┘
doc    └──────┘                          └┘
txt    └──────┘                          └┘
par    └──────┘                          └┘
pid    └───┘└─┘                          └┘
st   ──────────────────────────────────────────┘└─
279    rw [function.comp_app, function.comp_app, norm_mul, int.nat_abs_mul,
id         └───────────────┘  └───────────────┘  └──────┘  └─────────────┘
src    └──┘└───────────────┘└┘└───────────────┘└┘└──────┘└┘└─────────────┘└─
typ    └──┘└───────────────┘└┘└───────────────┘└┘└──────┘└┘└─────────────┘└─
doc    └──┘                 └┘                 └┘        └┘               └─
txt    └──┘                 └┘                 └┘        └┘               └─
par    └──┘                 └┘                 └┘        └┘               └─
pid      └┘                 └┘                 └┘        └┘               └─
st   ──────────────────────┘└─────────────────┘└────────┘└───────────────┘└─
280      norm_one, int.nat_abs_one, eq_comm, nat.mul_eq_one_iff] at this,
id       └──────┘  └─────────────┘  └─────┘  └────────────────┘
src  ───┘└──────┘└┘└─────────────┘└┘└─────┘└┘└────────────────┘└───────┘
typ  ───┘└──────┘└┘└─────────────┘└┘└─────┘└┘└────────────────┘└───────┘
doc  ───┘        └┘               └┘       └┘                  └───────┘
txt  ───┘        └┘               └┘       └┘                  └───────┘
par  ───┘        └┘               └┘       └┘                  └───────┘
pid  ───┘        └┘               └┘       └┘                  └──────┘
st   ───────────┘└───────────────┘└───────┘└──────────────────┘└──────┘└─
281    exact this.1
id           └──┘
src    └────┘    └─┘
typ    └────┘└──┘└─┘
doc    └────┘    └─┘
txt    └────┘    └─┘
par    └────┘    └─┘
pid             └─┘
st   ──────────────┘
282  end⟩
st   └─┘
283  
284  end norm
285  
286  end
287  
288  section
289  parameter {d : ℕ}
id                  
src                 
typ                 
290  
291    /-- Nonnegativity of an element of `ℤ√d`. -/
292    def nonneg : ℤ√d → Prop | ⟨a, b⟩ := nonnegg d 1 a b
id                  └┘                 └─────┘ 
src                 └┘                     └─────┘
typ                 └┘                 └─────┘ 
doc                 └┘                     └─────┘
293  
294    protected def le (a b : ℤ√d) : Prop := nonneg (b - a)
id                             └┘            └────┘    
src                            └┘             └────┘    
typ                            └┘            └────┘    
doc                            └┘             └────┘
295  
296    instance : has_le ℤ√d := ⟨zsqrtd.le⟩
id                └────┘ └┘     └───────┘
src               └────┘ └┘      └───────┘
typ               └────┘ └┘     └───────┘
doc                      └┘
297  
298    protected def lt (a b : ℤ√d) : Prop := ¬(b ≤ a)
id                             └┘               
src                            └┘                
typ                            └┘               
doc                            └┘
299  
300    instance : has_lt ℤ√d := ⟨zsqrtd.lt⟩
id                └────┘ └┘     └───────┘
src               └────┘ └┘      └───────┘
typ               └────┘ └┘     └───────┘
doc                      └┘
301  
302    instance decidable_nonnegg (c d a b) : decidable (nonnegg c d a b) :=
id                                            └───────┘  └─────┘    
src                                           └───────┘  └─────┘
typ                                           └───────┘  └─────┘    
doc                                                      └─────┘
303    by cases a; cases b; repeat {rw int.of_nat_eq_coe}; unfold nonnegg sq_le; apply_instance
id                                   └───────────────┘
src       └────┘   └────┘   └──────┘└─┘└───────────────┘  └──────────────────┘  └──────────────
typ       └────┘  └────┘  └──────┘└─┘└───────────────┘  └──────────────────┘  └──────────────
doc       └────┘   └────┘   └──────┘└─┘                   └──────────────────┘  └──────────────
txt       └────┘   └────┘   └──────┘└─┘                   └──────────────────┘  └──────────────
par       └────┘   └────┘   └──────┘└─┘                   └──────────────────┘  └──────────────
pid                             └───┘                         └────────────┘                
st       └─────────────────────────┘└──────────────────┘└┘└─────────────────────────────────────
304  
src  
typ  
doc  
txt  
par  
pid  
st   
305    instance decidable_nonneg : Π (a : ℤ√d), decidable (nonneg a)
id                                       └┘   └───────┘  └────┘ 
src  ─┘                                   └┘    └───────┘  └────┘
typ  ─┘                                  └┘   └───────┘  └────┘ 
doc  ─┘                                   └┘               └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
306    | ⟨a, b⟩ := zsqrtd.decidable_nonnegg _ _ _ _
id                 └──────────────────────┘
src                └──────────────────────┘
typ                └──────────────────────┘
307  
308    instance decidable_le (a b : ℤ√d) : decidable (a ≤ b) := decidable_nonneg _
id                                  └┘    └───────┘         └──────────────┘
src                                 └┘     └───────┘           └──────────────┘
typ                                 └┘    └───────┘         └──────────────┘
doc                                 └┘
309  
310    theorem nonneg_cases : Π {a : ℤ√d}, nonneg a → ∃ x y : ℕ, a = ⟨x, y⟩ ∨ a = ⟨x, -y⟩ ∨ a = ⟨-x, y⟩
id                                  └┘   └────┘                                 
src                                  └┘    └────┘                                       
typ                                 └┘   └────┘                                 
doc                                  └┘    └────┘
311    | ⟨(x : ℕ), (y : ℕ)⟩ h := ⟨x, y, or.inl rfl⟩
id                                  └────┘ └─┘
src                                   └────┘ └─┘
typ                                 └────┘ └─┘
312    | ⟨(x : ℕ), -[1+ y]⟩ h := ⟨x, y+1, or.inr $ or.inl rfl⟩
id               └──┘                └────┘   └────┘ └─┘
src               └──┘                 └────┘   └────┘ └─┘
typ              └──┘                └────┘   └────┘ └─┘
313    | ⟨-[1+ x], (y : ℕ)⟩ h := ⟨x+1, y, or.inr $ or.inr rfl⟩
id        └──┘                       └────┘   └────┘ └─┘
src       └──┘                         └────┘   └────┘ └─┘
typ       └──┘                       └────┘   └────┘ └─┘
314    | ⟨-[1+ x], -[1+ y]⟩ h := false.elim h
id        └──┘    └──┘        └────────┘
src       └──┘    └──┘         └────────┘
typ       └──┘    └──┘        └────────┘
315  
316    lemma nonneg_add_lem {x y z w : ℕ} (xy : nonneg ⟨x, -y⟩) (zw : nonneg ⟨-z, w⟩) : nonneg (⟨x, -y⟩ + ⟨-z, w⟩) :=
id                                             └────┘             └────┘         └────┘           
src                                            └────┘               └────┘           └────┘           
typ                                            └────┘             └────┘         └────┘           
doc                                             └────┘                └────┘            └────┘
317    have nonneg ⟨int.sub_nat_nat x z, int.sub_nat_nat w y⟩, from int.sub_nat_nat_elim x z
id          └────┘  └─────────────┘    └─────────────┘          └──────────────────┘  
src         └────┘  └─────────────┘      └─────────────┘            └──────────────────┘
typ         └────┘  └─────────────┘    └─────────────┘          └──────────────────┘  
doc         └────┘
318      (λm n i, sq_le y d m 1 → sq_le n 1 w d → nonneg ⟨i, int.sub_nat_nat w y⟩)
id             └───┘        └───┘        └────┘    └─────────────┘  
src               └───┘           └───┘           └────┘     └─────────────┘
typ            └───┘        └───┘        └────┘    └─────────────┘  
doc               └───┘           └───┘           └────┘
319      (λj k, int.sub_nat_nat_elim w y
id            └──────────────────┘  
src             └──────────────────┘
typ           └──────────────────┘  
320        (λm n i, sq_le n d (k + j) 1 → sq_le k 1 m d → nonneg ⟨int.of_nat j, i⟩)
id               └───┘            └───┘        └────┘  └────────┘   
src                 └───┘                └───┘           └────┘  └────────┘
typ              └───┘            └───┘        └────┘  └────────┘   
doc                 └───┘                 └───┘           └────┘
321        (λm n xy zw, trivial)
id             └┘ └┘  └─────┘
src                     └─────┘
typ            └┘ └┘  └─────┘
322        (λm n xy zw, sq_le_cancel zw xy))
id             └┘ └┘  └──────────┘ └┘ └┘
src                     └──────────┘
typ            └┘ └┘  └──────────┘ └┘ └┘
323      (λj k, int.sub_nat_nat_elim w y
id            └──────────────────┘  
src             └──────────────────┘
typ           └──────────────────┘  
324        (λm n i, sq_le n d k 1 → sq_le (k + j + 1) 1 m d → nonneg ⟨-[1+ j], i⟩)
id               └───┘        └───┘               └────┘  └──┘   
src                 └───┘           └───┘                   └────┘  └──┘  
typ              └───┘        └───┘               └────┘  └──┘   
doc                 └───┘           └───┘                     └────┘
325        (λm n xy zw, sq_le_cancel xy zw)
id             └┘ └┘  └──────────┘ └┘ └┘
src                     └──────────┘
typ            └┘ └┘  └──────────┘ └┘ └┘
326        (λm n xy zw, let t := nat.le_trans zw (sq_le_of_le (nat.le_add_right n (m+1)) (le_refl _) xy) in
id             └┘ └┘          └──────────┘ └┘  └─────────┘  └──────────────┘        └─────┘    └┘
src                              └──────────┘     └─────────┘  └──────────────┘          └─────┘
typ            └┘ └┘          └──────────┘ └┘  └─────────┘  └──────────────┘        └─────┘    └┘
327          have k + j + 1 ≤ k, from nat.mul_self_le_mul_self_iff.2 (by repeat{rw one_mul at t}; exact t),
id                              └──────────────────────────┘                └─────┘              
src                                └──────────────────────────┘      └─────┘└─┘└─────┘└───┘  └────┘
typ                             └──────────────────────────┘      └─────┘└─┘└─────┘└───┘  └────┘
doc                                                                      └─────┘└─┘       └───┘  └────┘
txt                                                                      └─────┘└─┘       └───┘  └────┘
par                                                                      └─────┘└─┘       └───┘  └────┘
pid                                                                            └──┘       └────┘       
st                                                                      └─────────────────────┘└┘└──────┘
328          absurd this (not_le_of_gt $ nat.succ_le_succ $ nat.le_add_right _ _))) (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw),
id           └────┘ └──┘  └──────────┘   └──────────────┘   └──────────────┘         └─────────────┘  └┘   └─────────────┘  └┘
src          └────┘       └──────────┘   └──────────────┘   └──────────────┘         └─────────────┘       └─────────────┘
typ          └────┘ └──┘  └──────────┘   └──────────────┘   └──────────────┘         └─────────────┘  └┘   └─────────────┘  └┘
329    show nonneg ⟨_, _⟩, by rw [neg_add_eq_sub]; rwa [int.sub_nat_nat_eq_coe,int.sub_nat_nat_eq_coe] at this
id          └────┘                └────────────┘        └────────────────────┘ └────────────────────┘
src         └────┘            └──┘└────────────┘  └───┘└────────────────────┘└────────────────────┘└─────────
typ         └────┘            └──┘└────────────┘  └───┘└────────────────────┘└────────────────────┘└─────────
doc         └────┘            └──┘                └───┘                                            └─────────
txt                           └──┘                └───┘                                            └─────────
par                           └──┘                └───┘                                            └─────────
pid                             └┘                   └┘                                            └──────┘
st                           └─────────────────┘└─────┘└────────────────────┘└─────────────────────┘└────────
330  
src  
typ  
doc  
txt  
par  
pid  
st   
331    theorem nonneg_add {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a + b) :=
id                               └┘        └────┘         └────┘     └────┘    
src  ─┘                          └┘         └────┘          └────┘      └────┘    
typ  ─┘                          └┘        └────┘         └────┘     └────┘    
doc  ─┘                          └┘         └────┘          └────┘      └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
332    begin
st     └─────
333      rcases nonneg_cases ha with ⟨x, y, rfl|rfl|rfl⟩;
id              └──────────┘ └┘
src      └─────┘└──────────┘  └───────────────────────┘
typ      └─────┘└──────────┘└┘└───────────────────────┘
doc      └─────┘              └───────────────────────┘
txt      └─────┘              └───────────────────────┘
par      └─────┘              └───────────────────────┘
pid                          └───────────────────────┘
st   ─────────────────────────────────────────────────────
334      rcases nonneg_cases hb with ⟨z, w, rfl|rfl|rfl⟩; dsimp [add, nonneg] at ha hb ⊢,
id              └──────────┘ └┘                                  └─┘  └────┘
src      └─────┘└──────────┘  └───────────────────────┘  └─────┘└─┘└┘└────┘└──────────┘
typ      └─────┘└──────────┘└┘└───────────────────────┘  └─────┘└─┘└┘└────┘└──────────┘
doc      └─────┘              └───────────────────────┘  └─────┘└─┘└┘└────┘└──────────┘
txt      └─────┘              └───────────────────────┘  └─────┘   └┘      └──────────┘
par      └─────┘              └───────────────────────┘  └─────┘   └┘      └──────────┘
pid                          └───────────────────────┘          └┘      └────────┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
335      { trivial },
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid               
st   ─────┘└──────┘└┘
336      { refine nonnegg_cases_right (λi h, sq_le_of_le _ _ (nonnegg_pos_neg.1 hb)),
id                └─────────────────┘        └─────────┘      └─────────────┘   └┘
src        └─────┘└─────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘  └┘
typ        └─────┘└─────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc        └─────┘                     └───┘           └───┘                └─┘  └┘
txt        └─────┘                     └───┘           └───┘                └─┘  └┘
par        └─────┘                     └───┘           └───┘                └─┘  └┘
pid                                   └───┘           └───┘                └─┘  └┘
st   ─────┘└───────────────────────────────────────────────────────────────────────┘└─
337        { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ y (by simp *))) },
id                 └────────────┘    └──────────────┘   └──────────┘     
src          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘    └────┘└──┘
typ          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘   └────┘└──┘
doc          └────┘              └─┘                               └───┘    └────┘└──┘
txt          └────┘              └─┘                               └───┘    └────┘└──┘
par          └────┘              └─┘                               └───┘    └────┘└──┘
pid                             └─┘                               └───┘    └────────┘
st   ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘
338        { apply nat.le_add_left } },
id                 └─────────────┘
src          └────┘└─────────────┘
typ          └────┘└─────────────┘
doc          └────┘               
txt          └────┘               
par          └────┘               
pid                              
st   ─────────────────────────────┘└──┘
339      { refine nonnegg_cases_left (λi h, sq_le_of_le _ _ (nonnegg_neg_pos.1 hb)),
id                └────────────────┘        └─────────┘      └─────────────┘   └┘
src        └─────┘└────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘  └┘
typ        └─────┘└────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc        └─────┘                    └───┘           └───┘                └─┘  └┘
txt        └─────┘                    └───┘           └───┘                └─┘  └┘
par        └─────┘                    └───┘           └───┘                └─┘  └┘
pid                                  └───┘           └───┘                └─┘  └┘
st   ─────┘└──────────────────────────────────────────────────────────────────────┘└─
340        { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ x (by simp *))) },
id                 └────────────┘    └──────────────┘   └──────────┘     
src          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘    └────┘└──┘
typ          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘   └────┘└──┘
doc          └────┘              └─┘                               └───┘    └────┘└──┘
txt          └────┘              └─┘                               └───┘    └────┘└──┘
par          └────┘              └─┘                               └───┘    └────┘└──┘
pid                             └─┘                               └───┘    └────────┘
st   ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘
341        { apply nat.le_add_left } },
id                 └─────────────┘
src          └────┘└─────────────┘
typ          └────┘└─────────────┘
doc          └────┘               
txt          └────┘               
par          └────┘               
pid                              
st   ─────────────────────────────┘└──┘
342      { refine nonnegg_cases_right (λi h, sq_le_of_le _ _ (nonnegg_pos_neg.1 ha)),
id                └─────────────────┘        └─────────┘      └─────────────┘   └┘
src        └─────┘└─────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘  └┘
typ        └─────┘└─────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc        └─────┘                     └───┘           └───┘                └─┘  └┘
txt        └─────┘                     └───┘           └───┘                └─┘  └┘
par        └─────┘                     └───┘           └───┘                └─┘  └┘
pid                                   └───┘           └───┘                └─┘  └┘
st   ─────┘└───────────────────────────────────────────────────────────────────────┘└─
343        { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ w (by simp *))) },
id                 └────────────┘    └──────────────┘   └──────────┘     
src          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘    └────┘└──┘
typ          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘   └────┘└──┘
doc          └────┘              └─┘                               └───┘    └────┘└──┘
txt          └────┘              └─┘                               └───┘    └────┘└──┘
par          └────┘              └─┘                               └───┘    └────┘└──┘
pid                             └─┘                               └───┘    └────────┘
st   ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘
344        { apply nat.le_add_right } },
id                 └──────────────┘
src          └────┘└──────────────┘
typ          └────┘└──────────────┘
doc          └────┘                
txt          └────┘                
par          └────┘                
pid                               
st   ──────────────────────────────┘└──┘
345      { simpa using nonnegg_pos_neg.2 (sq_le_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb)) },
id                                        └───────┘                    └┘   └─────────────┘   └┘
src        └──────────┘               └─┘ └───────┘                └─┘  └┘ └─────────────┘└─┘  └─┘
typ        └──────────┘               └─┘ └───────┘                └─┘└┘└┘ └─────────────┘└─┘└┘└─┘
doc        └──────────┘               └─┘                          └─┘  └┘                └─┘  └─┘
txt        └──────────┘               └─┘                          └─┘  └┘                └─┘  └─┘
par        └──────────┘               └─┘                          └─┘  └┘                └─┘  └─┘
pid             └────┘               └─┘                          └─┘  └┘                └─┘  └┘
st   ─────┘└──────────────────────────────────────────────────────────────────────────────────────┘└┘
346      { exact nonneg_add_lem ha hb },
id               └────────────┘ └┘ └┘
src        └────┘└────────────┘    
typ        └────┘└────────────┘└┘└┘
doc        └────┘                  
txt        └────┘                  
par        └────┘                  
pid                               
st   ─────┘└─────────────────────────┘└┘
347      { refine nonnegg_cases_left (λi h, sq_le_of_le _ _ (nonnegg_neg_pos.1 ha)),
id                └────────────────┘        └─────────┘      └─────────────┘   └┘
src        └─────┘└────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘  └┘
typ        └─────┘└────────────────┘  └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc        └─────┘                    └───┘           └───┘                └─┘  └┘
txt        └─────┘                    └───┘           └───┘                └─┘  └┘
par        └─────┘                    └───┘           └───┘                └─┘  └┘
pid                                  └───┘           └───┘                └─┘  └┘
st   ─────┘└──────────────────────────────────────────────────────────────────────┘└─
348        { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ z (by simp *))) },
id                 └────────────┘    └──────────────┘   └──────────┘     
src          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘    └────┘└──┘
typ          └────┘└────────────┘└─┘ └──────────────┘  └──────────┘└───┘   └────┘└──┘
doc          └────┘              └─┘                               └───┘    └────┘└──┘
txt          └────┘              └─┘                               └───┘    └────┘└──┘
par          └────┘              └─┘                               └───┘    └────┘└──┘
pid                             └─┘                               └───┘    └────────┘
st   ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘
349        { apply nat.le_add_right } },
id                 └──────────────┘
src          └────┘└──────────────┘
typ          └────┘└──────────────┘
doc          └────┘                
txt          └────┘                
par          └────┘                
pid                               
st   ──────────────────────────────┘└──┘
350      { rw [add_comm, add_comm ↑y], exact nonneg_add_lem hb ha },
id             └──────┘  └──────┘          └────────────┘ └┘ └┘
src        └──┘└──────┘└┘└──────┘   └────┘└────────────┘    
typ        └──┘└──────┘└┘└──────┘  └────┘└────────────┘└┘└┘
doc        └──┘        └┘            └────┘                  
txt        └──┘        └┘            └────┘                  
par        └──┘        └┘            └────┘                  
pid          └┘        └┘                                   
st   ─────┘└──────────┘└───────────┘└────────────────────────────┘└┘
351      { simpa using nonnegg_neg_pos.2 (sq_le_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb)) },
id                                        └───────┘                    └┘   └─────────────┘   └┘
src        └──────────┘               └─┘ └───────┘                └─┘  └┘ └─────────────┘└─┘  └─┘
typ        └──────────┘               └─┘ └───────┘                └─┘└┘└┘ └─────────────┘└─┘└┘└─┘
doc        └──────────┘               └─┘                          └─┘  └┘                └─┘  └─┘
txt        └──────────┘               └─┘                          └─┘  └┘                └─┘  └─┘
par        └──────────┘               └─┘                          └─┘  └┘                └─┘  └─┘
pid             └────┘               └─┘                          └─┘  └┘                └─┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘└──
352    end
st   ────┘
353  
354    theorem le_refl (a : ℤ√d) : a ≤ a := show nonneg (a - a), by simp
id                          └┘               └────┘    
src                         └┘                  └────┘            └────
typ                         └┘               └────┘          └────
doc                         └┘                   └────┘             └────
txt                                                                 └────
par                                                                 └────
pid                                                                     
st                                                                 └─────
355  
src  
typ  
doc  
txt  
par  
pid  
st   
356    protected theorem le_trans {a b c : ℤ√d} (ab : a ≤ b) (bc : b ≤ c) : a ≤ c :=
id                                         └┘                          
src  ─┘                                    └┘                               
typ  ─┘                                    └┘                          
doc  ─┘                                    └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
357    have nonneg (b - a + (c - b)), from nonneg_add ab bc,
id          └────┘                  └────────┘ └┘ └┘
src         └────┘                      └────────┘
typ         └────┘                  └────────┘ └┘ └┘
doc         └────┘
358    by simpa
src       └─────
typ       └─────
doc       └─────
txt       └─────
par       └─────
pid            
st       └──────
359  
src  
typ  
doc  
txt  
par  
pid  
st   
360    theorem nonneg_iff_zero_le {a : ℤ√d} : nonneg a ↔ 0 ≤ a := show _ ↔ nonneg _, by simp
id                                     └┘    └────┘                  └────┘
src  ─┘                                └┘     └────┘                    └────┘       └────
typ  ─┘                                └┘    └────┘                  └────┘       └────
doc  ─┘                                └┘     └────┘                       └────┘       └────
txt  ─┘                                                                                 └────
par  ─┘                                                                                 └────
pid  ─┘                                                                                     
st   ─┘                                                                                └─────
361  
src  
typ  
doc  
txt  
par  
pid  
st   
362    theorem le_of_le_le {x y z w : ℤ} (xz : x ≤ z) (yw : y ≤ w) : (⟨x, y⟩ : ℤ√d) ≤ ⟨z, w⟩ :=
id                                                                    └┘      
src  ─┘                                                                     └┘   
typ  ─┘                                                               └┘      
doc  ─┘                                                                        └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
363    show nonneg ⟨z - x, w - y⟩, from
id          └────┘        
src         └────┘          
typ         └────┘        
doc         └────┘
364    match z - x, w - y, int.le.dest_sub xz, int.le.dest_sub yw with ._, ._, ⟨a, rfl⟩, ⟨b, rfl⟩ := trivial end
id                   └─────────────┘ └┘  └─────────────┘ └┘                            └─┘     └─────┘
src                      └─────────────┘     └─────────────┘                               └─┘     └─────┘
typ                  └─────────────┘ └┘  └─────────────┘ └┘                            └─┘     └─────┘
365  
366    theorem le_arch (a : ℤ√d) : ∃n : ℕ, a ≤ n :=
id                          └┘           
src                         └┘            
typ                         └┘           
doc                         └┘
367    let ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ := show ∃x y : ℕ, nonneg (⟨x, y⟩ + -a), from match -a with
id     └─┘                                       └────┘                      
src                                               └────┘                         
typ    └─┘                                       └────┘                      
doc                                                   └────┘
368    | ⟨int.of_nat x, int.of_nat y⟩ := ⟨0, 0, trivial⟩
id                      └────────┘              └─────┘
src                     └────────┘              └─────┘
typ                     └────────┘              └─────┘
369    | ⟨int.of_nat x, -[1+ y]⟩      := ⟨0, y+1, by simp [int.neg_succ_of_nat_coe]⟩
id        └────────┘    └──┘                            └─────────────────────┘
src       └────────┘    └──┘                       └────┘└─────────────────────┘
typ       └────────┘    └──┘                      └────┘└─────────────────────┘
doc                                                  └────┘                       
txt                                                  └────┘                       
par                                                  └────┘                       
pid                                                                             
st                                                  └─────────────────────────────┘
370    | ⟨-[1+ x],      int.of_nat y⟩ := ⟨x+1, 0, by simp [int.neg_succ_of_nat_coe]⟩
id        └──┘        └────────┘                        └─────────────────────┘
src       └──┘         └────────┘                  └────┘└─────────────────────┘
typ       └──┘        └────────┘                  └────┘└─────────────────────┘
doc                                                  └────┘                       
txt                                                  └────┘                       
par                                                  └────┘                       
pid                                                                             
st                                                  └─────────────────────────────┘
371    | ⟨-[1+ x],      -[1+ y]⟩      := ⟨x+1, y+1, by simp [int.neg_succ_of_nat_coe]⟩
id        └──┘        └──┘                             └─────────────────────┘
src       └──┘         └──┘                        └────┘└─────────────────────┘
typ       └──┘        └──┘                       └────┘└─────────────────────┘
doc                                                    └────┘                       
txt                                                    └────┘                       
par                                                    └────┘                       
pid                                                                               
st                                                    └─────────────────────────────┘
372    end in begin
st            └─────
373      refine ⟨x + d*y, zsqrtd.le_trans h _⟩,
id                                   
src      └─────┘    └┘                └─┘
typ      └─────┘ └┘               └─┘
doc      └─────┘      └┘                └─┘
txt      └─────┘      └┘                └─┘
par      └─────┘      └┘                └─┘
pid                  └┘                └─┘
st   ────────────────────────────────────────┘└─
374      rw [← int.cast_coe_nat, ← of_int_eq_coe],
id             └──────────────┘    └───────────┘
src      └────┘└──────────────┘└──┘└───────────┘
typ      └────┘└──────────────┘└──┘└───────────┘
doc      └────┘                └──┘             
txt      └────┘                └──┘             
par      └────┘                └──┘             
pid        └──┘                └──┘             
st   ─────────────────────────┘└───────────────┘└──
375      change nonneg ⟨(↑x + d*y) - ↑x, 0-↑y⟩,
id              └────┘                  
src      └─────┘└────┘       └┘  └─┘   
typ      └─────┘└────┘      └┘ └─┘  
doc      └─────┘└────┘        └┘   └─┘   
txt      └─────┘              └┘   └─┘   
par      └─────┘              └┘   └─┘   
pid                          └┘   └─┘   
st   ────────────────────────────────────────┘└─
376      cases y with y,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
377      { simp },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
378      have h : ∀y, sq_le y d (d * y) 1 := λ y,
id                    └───┘      
src      └───────┘  └───┘      └─────┘ └───
typ      └───────┘  └───┘     └─────┘ └───
doc      └───────┘  └───┘      └─────┘ └───
txt      └───────┘             └─────┘ └───
par      └───────┘             └─────┘ └───
pid      └────┘└─┘             └┘└───┘ └───
st   ─────────────────────────────────────────────
379        by simpa [sq_le, mul_comm, mul_left_comm] using
id                   └───┘  └──────┘  └───────────┘
src  ─────┘  └─────┘└───┘└┘└──────┘└┘└───────────┘└───────
typ  ─────┘  └─────┘└───┘└┘└──────┘└┘└───────────┘└───────
doc  ─────┘  └─────┘└───┘└┘        └┘             └───────
txt  ─────┘  └─────┘     └┘        └┘             └───────
par  ─────┘  └─────┘     └┘        └┘             └───────
pid  ─────┘  └──────┘     └┘        └┘             └───────
st   ───────┘└─────────────────────────────────────────────
380           nat.mul_le_mul_right (y * y) (nat.le_mul_self d),
id            └──────────────────┘         └─────────────┘ 
src  ────────┘└──────────────────┘    └┘ └─────────────┘ 
typ  ────────┘└──────────────────┘   └┘ └─────────────┘
doc  ────────┘                        └┘                 
txt  ────────┘                        └┘                 
par  ────────┘                        └┘                 
pid  ────────┘                        └┘                 
st   ────────────────────────────────────────────────────────┘└─
381      rw [show (x:ℤ) + d * nat.succ y - x = d * nat.succ y, by simp],
id                                              └──────┘ 
src      └──┘       └┘                └──────┘ └───┘└──┘
typ      └──┘       └┘              └──────┘└───┘└──┘
doc      └──┘       └┘                          └───┘└──┘
txt      └──┘       └┘                          └───┘└──┘
par      └──┘       └┘                          └───┘└──┘
pid        └┘       └┘                          └────────┘
st   ───────────────────────────────────────────────────────────┘└───┘└──
382      exact h (y+1)
id               
src      └────┘    └──
typ      └────┘  └──
doc      └────┘    └──
txt      └────┘    └──
par      └────┘    └──
pid               └┘
st   ──────────────────
383    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
384  
385    protected theorem nonneg_total : Π (a : ℤ√d), nonneg a ∨ nonneg (-a)
id                                            └┘   └────┘   └────┘  
src                                            └┘    └────┘    └────┘  
typ                                           └┘   └────┘   └────┘  
doc                                            └┘    └────┘     └────┘
386    | ⟨(x : ℕ), (y : ℕ)⟩ := or.inl trivial
id                           └────┘ └─────┘
src                          └────┘ └─────┘
typ                          └────┘ └─────┘
387    | ⟨-[1+ x], -[1+ y]⟩ := or.inr trivial
id        └──┘    └──┘       └────┘ └─────┘
src       └──┘    └──┘       └────┘ └─────┘
typ       └──┘    └──┘       └────┘ └─────┘
388    | ⟨0,       -[1+ y]⟩ := or.inr trivial
id                 └──┘       └────┘ └─────┘
src                └──┘       └────┘ └─────┘
typ                └──┘       └────┘ └─────┘
389    | ⟨-[1+ x], 0⟩       := or.inr trivial
id        └──┘                └────┘ └─────┘
src       └──┘                └────┘ └─────┘
typ       └──┘                └────┘ └─────┘
390    | ⟨(x+1:ℕ), -[1+ y]⟩ := nat.le_total
id               └──┘       └──────────┘
src              └──┘       └──────────┘
typ              └──┘       └──────────┘
391    | ⟨-[1+ x], (y+1:ℕ)⟩ := nat.le_total
id        └──┘              └──────────┘
src       └──┘              └──────────┘
typ       └──┘              └──────────┘
392  
393    protected theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a :=
id                                       └┘          
src                                      └┘             
typ                                      └┘          
doc                                      └┘
394    let t := nonneg_total (b - a) in by rw [show -(b-a) = a-b, from neg_sub b a] at t; exact t
id             └──────────┘                                     └─────┘                
src             └──────────┘              └──┘       └┘   └─────┘└─────┘  └────┘  └────┘ 
typ            └──────────┘            └──┘       └┘   └─────┘└─────┘└────┘  └────┘
doc                                        └──┘         └┘    └─────┘         └────┘  └────┘ 
txt                                        └──┘         └┘    └─────┘         └────┘  └────┘ 
par                                        └──┘         └┘    └─────┘         └────┘  └────┘ 
pid                                          └┘         └┘    └─────┘         └───┘        
st                                        └──────────────────────────────────────┘└──────────────
395  
src  
typ  
doc  
txt  
par  
pid  
st   
396    instance : preorder ℤ√d :=
id                └──────┘ └┘
src  ─┘           └──────┘ └┘
typ  ─┘           └──────┘ └┘
doc  ─┘                    └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
397    { le               := zsqrtd.le,
id                           └───────┘
src                          └───────┘
typ                          └───────┘
398      le_refl          := zsqrtd.le_refl,
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
399      le_trans         := @zsqrtd.le_trans,
id                            └─────────────┘
src                           └─────────────┘
typ                           └─────────────┘
400      lt               := zsqrtd.lt,
id                           └───────┘
src                          └───────┘
typ                          └───────┘
401      lt_iff_le_not_le := λ a b,
id                              
typ                             
402        (and_iff_right_of_imp (zsqrtd.le_total _ _).resolve_left).symm }
id          └──────────────────┘  └─────────────┘     └──────────┘  └──┘
src         └──────────────────┘  └─────────────┘     └──────────┘  └──┘
typ         └──────────────────┘  └─────────────┘     └──────────┘  └──┘
403  
404    protected theorem add_le_add_left (a b : ℤ√d) (ab : a ≤ b) (c : ℤ√d) : c + a ≤ c + b :=
id                                              └┘                 └┘          
src                                             └┘                    └┘             
typ                                             └┘                 └┘          
doc                                             └┘                     └┘
405    show nonneg _, by rw add_sub_add_left_eq_sub; exact ab
id          └────┘          └─────────────────────┘        └┘
src         └────┘       └─┘└─────────────────────┘  └────┘  
typ         └────┘       └─┘└─────────────────────┘  └────┘└┘
doc         └────┘       └─┘                         └────┘  
txt                      └─┘                         └────┘  
par                      └─┘                         └────┘  
pid                                                        
st                      └─────────────────────────────────────
406  
src  
typ  
doc  
txt  
par  
pid  
st   
407    protected theorem le_of_add_le_add_left (a b c : ℤ√d) (h : c + a ≤ c + b) : a ≤ b :=
id                                                      └┘                   
src  ─┘                                                 └┘                        
typ  ─┘                                                 └┘                   
doc  ─┘                                                 └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
408    by simpa using zsqrtd.add_le_add_left _ _ h (-c)
id                                                 
src       └──────────┘                      └───┘   └─
typ       └──────────┘                      └───┘ └─
doc       └──────────┘                      └───┘    └─
txt       └──────────┘                      └───┘    └─
par       └──────────┘                      └───┘    └─
pid            └────┘                      └───┘    
st       └──────────────────────────────────────────────
409  
src  
typ  
doc  
txt  
par  
pid  
st   
410    protected theorem add_lt_add_left (a b : ℤ√d) (h : a < b) (c) : c + a < c + b :=
id                                              └┘                       
src  ─┘                                         └┘                            
typ  ─┘                                         └┘                       
doc  ─┘                                         └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
411    λ h', h (zsqrtd.le_of_add_le_add_left _ _ _ h')
id       └┘    └──────────────────────────┘       └┘
src             └──────────────────────────┘
typ      └┘    └──────────────────────────┘       └┘
412  
413    theorem nonneg_smul {a : ℤ√d} {n : ℕ} (ha : nonneg a) : nonneg (n * a) :=
id                              └┘               └────┘     └────┘    
src                             └┘                └────┘      └────┘    
typ                             └┘               └────┘     └────┘    
doc                             └┘                 └────┘      └────┘
414    by rw ← int.cast_coe_nat; exact match a, nonneg_cases ha, ha with
id             └──────────────┘                └──────────┘     └┘
src       └───┘└──────────────┘  └────┘      └┘└──────────┘  └┘  └─────
typ       └───┘└──────────────┘  └────┘     └┘└──────────┘  └┘└┘└─────
doc       └───┘                  └────┘      └┘              └┘  └─────
txt       └───┘                  └────┘      └┘              └┘  └─────
par       └───┘                  └────┘      └┘              └┘  └─────
pid         └─┘                             └┘              └┘  └─────
st       └───────────────────────────────────────────────────────────────
415    | ._, ⟨x, y, or.inl rfl⟩,          ha := by rw smul_val; trivial
id                  └────┘ └─┘                        └──────┘
src  ───┘  └┘  └┘ └┘└────┘└─┘└──────────┘  └──┘  └─┘└──────┘└┘└───────
typ  ───┘  └┘  └┘ └┘└────┘└─┘└──────────┘  └──┘  └─┘└──────┘└┘└───────
doc  ───┘  └┘  └┘ └┘         └──────────┘  └──┘  └─┘        └┘└───────
txt  ───┘  └┘  └┘ └┘         └──────────┘  └──┘  └─┘        └┘└───────
par  ───┘  └┘  └┘ └┘         └──────────┘  └──┘  └─┘        └┘└───────
pid  ───┘  └┘  └┘ └┘         └──────────┘  └──┘  └──┘        └─────────
st   ────────────────────────────────────────────┘└─────────────────────
416    | ._, ⟨x, y, or.inr $ or.inl rfl⟩, ha := by rw smul_val; simpa using
id                  └────┘                            └──────┘
src  ─┘└┘  └┘  └┘ └┘└────┘          └─┘  └──┘  └─┘└──────┘└┘└───────────
typ  ─┘└┘  └┘  └┘ └┘└────┘          └─┘  └──┘  └─┘└──────┘└┘└───────────
doc  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘        └┘└───────────
txt  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘        └┘└───────────
par  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘        └┘└───────────
pid  ───┘  └┘  └┘ └┘                └─┘  └──┘  └──┘        └─────────────
st   ─┘└─────────────────────────────────────────┘└─────────────────────────
417      nonnegg_pos_neg.2 (sq_le_smul n $ nonnegg_pos_neg.1 ha)
id                          └────────┘    └─────────────┘   └┘
src  ───┘               └─┘ └────────┘  └─────────────┘└─┘  └─
typ  ───┘               └─┘ └────────┘ └─────────────┘└─┘└┘└─
doc  ───┘               └─┘                            └─┘  └─
txt  ───┘               └─┘                            └─┘  └─
par  ───┘               └─┘                            └─┘  └─
pid  ───┘               └─┘                            └─┘  └─
st   ────────────────────────────────────────────────────────────
418    | ._, ⟨x, y, or.inr $ or.inr rfl⟩, ha := by rw smul_val; simpa using
id                                                    └──────┘
src  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘└──────┘└┘└───────────
typ  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘└──────┘└┘└───────────
doc  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘        └┘└───────────
txt  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘        └┘└───────────
par  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └─┘        └┘└───────────
pid  ───┘  └┘  └┘ └┘                └─┘  └──┘  └──┘        └─────────────
st   ─┘└─────────────────────────────────────────┘└─────────────────────────
419      nonnegg_neg_pos.2 (sq_le_smul n $ nonnegg_neg_pos.1 ha)
id                          └────────┘    └─────────────┘   └┘
src  ───┘               └─┘ └────────┘  └─────────────┘└─┘  └─
typ  ───┘               └─┘ └────────┘ └─────────────┘└─┘└┘└─
doc  ───┘               └─┘                            └─┘  └─
txt  ───┘               └─┘                            └─┘  └─
par  ───┘               └─┘                            └─┘  └─
pid  ───┘               └─┘                            └─┘  └─
st   ────────────────────────────────────────────────────────────
420    end
src  ─┘└───
typ  ─┘└───
doc  ─┘└───
txt  ─┘└───
par  ─┘└───
pid  ────┘
st   ─┘└───
421  
src  
typ  
doc  
txt  
par  
pid  
st   
422    theorem nonneg_muld {a : ℤ√d} (ha : nonneg a) : nonneg (sqrtd * a) :=
id                              └┘        └────┘     └────┘  └───┘  
src  ─┘                         └┘         └────┘      └────┘  └───┘ 
typ  ─┘                         └┘        └────┘     └────┘  └───┘  
doc  ─┘                         └┘         └────┘      └────┘  └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
423    by refine match a, nonneg_cases ha, ha with
id                       └──────────┘     └┘
src       └─────┘      └┘└──────────┘  └┘  └─────
typ       └─────┘     └┘└──────────┘  └┘└┘└─────
doc       └─────┘      └┘              └┘  └─────
txt       └─────┘      └┘              └┘  └─────
par       └─────┘      └┘              └┘  └─────
pid                   └┘              └┘  └─────
st       └─────────────────────────────────────────
424    | ._, ⟨x, y, or.inl rfl⟩,          ha := trivial
id                  └────┘ └─┘                  └─────┘
src  ───┘  └┘  └┘ └┘└────┘└─┘└──────────┘  └──┘└─────┘
typ  ───┘  └┘  └┘ └┘└────┘└─┘└──────────┘  └──┘└─────┘
doc  ───┘  └┘  └┘ └┘         └──────────┘  └──┘       
txt  ───┘  └┘  └┘ └┘         └──────────┘  └──┘       
par  ───┘  └┘  └┘ └┘         └──────────┘  └──┘       
pid  ───┘  └┘  └┘ └┘         └──────────┘  └──┘       
st   ───────────────────────────────────────────────────
425    | ._, ⟨x, y, or.inr $ or.inl rfl⟩, ha := by simp; apply nonnegg_neg_pos.2;
id                  └────┘                                     └─────────────┘
src  ───┘  └┘  └┘ └┘└────┘          └─┘  └──┘  └──┘└┘└────┘└─────────────┘└┘└─
typ  ───┘  └┘  └┘ └┘└────┘          └─┘  └──┘  └──┘└──────┘└─────────────┘└───
doc  ───┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└┘└────┘               └┘└─
txt  ───┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└┘└────┘               └┘└─
par  ───┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└──────┘               └───
pid  ───┘  └┘  └┘ └┘                └─┘  └──┘  └───────────┘               └───
st   ────────────────────────────────────────────┘└───────────────────────────────
426      simpa [sq_le, mul_comm, mul_left_comm] using
id              └───┘  └──────┘  └───────────┘
src  ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
typ  ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
doc  ───┘└─────┘└───┘└┘        └┘             └───────
txt  ───┘└─────┘     └┘        └┘             └───────
par  ───┘└─────┘     └┘        └┘             └───────
pid  ──────────┘     └┘        └┘             └───────
st   ─────────────────────────────────────────────────
427        nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)
id         └─────────────────┘   └─────────────┘   └┘
src  ─────┘└─────────────────┘  └─────────────┘└─┘  └─
typ  ─────┘└─────────────────┘ └─────────────┘└─┘└┘└─
doc  ─────┘                                    └─┘  └─
txt  ─────┘                                    └─┘  └─
par  ─────┘                                    └─┘  └─
pid  ─────┘                                    └─┘  └─
st   ───────────────────────────────────────────────────
428    | ._, ⟨x, y, or.inr $ or.inr rfl⟩, ha := by simp; apply nonnegg_pos_neg.2;
id                                                             └─────────────┘
src  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└┘└────┘└─────────────┘└┘└─
typ  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└──────┘└─────────────┘└───
doc  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└┘└────┘               └┘└─
txt  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└┘└────┘               └┘└─
par  ─┘└┘  └┘  └┘ └┘                └─┘  └──┘  └──┘└──────┘               └───
pid  ───┘  └┘  └┘ └┘                └─┘  └──┘  └───────────┘               └───
st   ─┘└─────────────────────────────────────────┘└───────────────────────────────
429      simpa [sq_le, mul_comm, mul_left_comm] using
id              └───┘  └──────┘  └───────────┘
src  ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
typ  ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
doc  ───┘└─────┘└───┘└┘        └┘             └───────
txt  ───┘└─────┘     └┘        └┘             └───────
par  ───┘└─────┘     └┘        └┘             └───────
pid  ──────────┘     └┘        └┘             └───────
st   ─────────────────────────────────────────────────
430        nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)
id         └─────────────────┘   └─────────────┘   └┘
src  ─────┘└─────────────────┘  └─────────────┘└─┘  └─
typ  ─────┘└─────────────────┘ └─────────────┘└─┘└┘└─
doc  ─────┘                                    └─┘  └─
txt  ─────┘                                    └─┘  └─
par  ─────┘                                    └─┘  └─
pid  ─────┘                                    └─┘  └─
st   ───────────────────────────────────────────────────
431    end
src  ─┘└───
typ  ─┘└───
doc  ─┘└───
txt  ─┘└───
par  ─┘└───
pid  ────┘
st   ─┘└───
432  
src  
typ  
doc  
txt  
par  
pid  
st   
433    theorem nonneg_mul_lem {x y : ℕ} {a : ℤ√d} (ha : nonneg a) : nonneg (⟨x, y⟩ * a) :=
id                                          └┘        └────┘     └────┘        
src  ─┘                                     └┘         └────┘      └────┘         
typ  ─┘                                     └┘        └────┘     └────┘        
doc  ─┘                                      └┘         └────┘      └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
434    have (⟨x, y⟩ * a : ℤ√d) = x * a + sqrtd * (y * a), by rw [decompose, right_distrib, mul_assoc]; refl,
id                    └┘       └───┘               └───────┘  └───────────┘  └───────┘
src                      └┘          └───┘             └──┘└───────┘└┘└───────────┘└┘└───────┘  └──┘
typ                   └┘       └───┘           └──┘└───────┘└┘└───────────┘└┘└───────┘  └──┘
doc                       └┘             └───┘               └──┘         └┘             └┘           └──┘
txt                                                          └──┘         └┘             └┘           └──┘
par                                                          └──┘         └┘             └┘           └──┘
pid                                                            └┘         └┘             └┘         
st                                                          └────────────┘└─────────────┘└─────────┘└────┘
435    by rw this; exact nonneg_add (nonneg_smul ha) (nonneg_muld $ nonneg_smul ha)
id           └──┘        └────────┘                   └─────────┘   └─────────┘ └┘
src       └─┘      └────┘└────────┘              └┘ └─────────┘ └─────────┘  └─
typ       └─┘└──┘  └────┘└────────┘              └┘ └─────────┘ └─────────┘└┘└─
doc       └─┘      └────┘                        └┘                          └─
txt       └─┘      └────┘                        └┘                          └─
par       └─┘      └────┘                        └┘                          └─
pid                                            └┘                          
st       └──────────────────────────────────────────────────────────────────────────
436  
src  
typ  
doc  
txt  
par  
pid  
st   
437    theorem nonneg_mul {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a * b) :=
id                               └┘        └────┘         └────┘     └────┘    
src  ─┘                          └┘         └────┘          └────┘      └────┘    
typ  ─┘                          └┘        └────┘         └────┘     └────┘    
doc  ─┘                          └┘         └────┘          └────┘      └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
438    match a, b, nonneg_cases ha, nonneg_cases hb, ha, hb with
id               └──────────┘ └┘  └──────────┘ └┘  └┘  └┘
src                └──────────┘     └──────────┘
typ              └──────────┘ └┘  └──────────┘ └┘  └┘  └┘
439    | ._, ._, ⟨x, y, or.inl rfl⟩,          ⟨z, w, or.inl rfl⟩,          ha, hb := trivial
id                                                   └────┘ └─┘                      └─────┘
src                                                  └────┘ └─┘                      └─────┘
typ                                                  └────┘ └─┘                      └─────┘
440    | ._, ._, ⟨x, y, or.inl rfl⟩,          ⟨z, w, or.inr $ or.inr rfl⟩, ha, hb := nonneg_mul_lem hb
id                      └────┘                                └────┘ └─┘       └┘    └────────────┘
src                     └────┘                                └────┘ └─┘             └────────────┘
typ                     └────┘                                └────┘ └─┘       └┘    └────────────┘
441    | ._, ._, ⟨x, y, or.inl rfl⟩,          ⟨z, w, or.inr $ or.inl rfl⟩, ha, hb := nonneg_mul_lem hb
id                                                   └────┘   └────┘ └─┘       └┘    └────────────┘
src                                                  └────┘   └────┘ └─┘             └────────────┘
typ                                                  └────┘   └────┘ └─┘       └┘    └────────────┘
442    | ._, ._, ⟨x, y, or.inr $ or.inr rfl⟩, ⟨z, w, or.inl rfl⟩,          ha, hb := by rw mul_comm; exact nonneg_mul_lem ha
id                               └────┘              └────┘ └─┘                            └──────┘        └────────────┘ └┘
src                              └────┘              └────┘ └─┘                         └─┘└──────┘  └────┘└────────────┘  
typ                              └────┘              └────┘ └─┘                         └─┘└──────┘  └────┘└────────────┘└┘
doc                                                                                     └─┘          └────┘                
txt                                                                                     └─┘          └────┘                
par                                                                                     └─┘          └────┘                
pid                                                                                                                      
st                                                                                     └─────────────────────────────────────
443    | ._, ._, ⟨x, y, or.inr $ or.inl rfl⟩, ⟨z, w, or.inl rfl⟩,          ha, hb := by rw mul_comm; exact nonneg_mul_lem ha
id                      └────┘                       └────┘ └─┘                            └──────┘        └────────────┘ └┘
src  ─┘                 └────┘                       └────┘ └─┘                         └─┘└──────┘  └────┘└────────────┘  
typ  ─┘                 └────┘                       └────┘ └─┘                         └─┘└──────┘  └────┘└────────────┘└┘
doc  ─┘                                                                                 └─┘          └────┘                
txt  ─┘                                                                                 └─┘          └────┘                
par  ─┘                                                                                 └─┘          └────┘                
pid  ─┘                                                                                                                  
st   ─┘                                                                                └─────────────────────────────────────
444    | ._, ._, ⟨x, y, or.inr $ or.inr rfl⟩, ⟨z, w, or.inr $ or.inr rfl⟩, ha, hb :=
id                                                            └────┘ └─┘
src  ─┘                                                       └────┘ └─┘
typ  ─┘                                                       └────┘ └─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
445      by rw [calc (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id                                                      └─┘
src         └──┘       └┘ └┘   └┘ └──┘   └┘  └──────┘└─┘
typ         └──┘       └┘ └┘   └┘ └──┘   └┘  └──────┘└─┘
doc         └──┘        └┘ └┘    └┘ └──┘   └┘  └──────┘   
txt         └──┘        └┘ └┘    └┘ └──┘   └┘  └──────┘   
par         └──┘        └┘ └┘    └┘ └──┘   └┘  └──────┘   
pid           └┘        └┘ └┘    └┘ └──┘   └┘  └──────┘   
st         └──────────────────────────────────────────────────
446          ... = ⟨x * z + d * y * w, -(x * w + y * z)⟩ : by simp]; exact
id                                              
src  ───────────┘          └┘         └───┘  └──┘  └─────
typ  ───────────┘         └┘     └───┘  └──┘  └─────
doc  ───────────┘           └┘         └───┘  └──┘  └─────
txt  ───────────┘           └┘         └───┘  └──┘  └─────
par  ───────────┘           └┘         └───┘  └──┘  └─────
pid  ───────────┘           └┘         └───┘  └────┘       
st   ───────────────────────────────────────────────────────┘└───┘└───────
447      nonnegg_pos_neg.2 (sq_le_mul.left (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
id       └─────────────┘    └────────────┘                    └┘   └─────────────┘   └┘
src  ───┘└─────────────┘└─┘ └────────────┘                └─┘  └┘ └─────────────┘└─┘  └──
typ  ───┘└─────────────┘└─┘ └────────────┘                └─┘└┘└┘ └─────────────┘└─┘└┘└──
doc  ───┘               └─┘                               └─┘  └┘                └─┘  └──
txt  ───┘               └─┘                               └─┘  └┘                └─┘  └──
par  ───┘               └─┘                               └─┘  └┘                └─┘  └──
pid  ───┘               └─┘                               └─┘  └┘                └─┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────────────
448    | ._, ._, ⟨x, y, or.inr $ or.inr rfl⟩, ⟨z, w, or.inr $ or.inl rfl⟩, ha, hb :=
id                                                   └────┘   └────┘ └─┘
src  ─┘                                              └────┘   └────┘ └─┘
typ  ─┘                                              └────┘   └────┘ └─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
449      by rw [calc (⟨-x, y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id                                                        └─┘
src         └──┘        └┘ └┘   └┘  └──┘   └┘  └──────┘└─┘
typ         └──┘        └┘ └┘   └┘  └──┘   └┘  └──────┘└─┘
doc         └──┘        └┘ └┘   └┘  └──┘   └┘  └──────┘   
txt         └──┘        └┘ └┘   └┘  └──┘   └┘  └──────┘   
par         └──┘        └┘ └┘   └┘  └──┘   └┘  └──────┘   
pid           └┘        └┘ └┘   └┘  └──┘   └┘  └──────┘   
st         └──────────────────────────────────────────────────
450          ... = ⟨-(x * z + d * y * w), x * w + y * z⟩ : by simp]; exact
id                                                
src  ───────────┘             └─┘       └──┘  └──┘  └─────
typ  ───────────┘            └─┘   └──┘  └──┘  └─────
doc  ───────────┘             └─┘       └──┘  └──┘  └─────
txt  ───────────┘             └─┘       └──┘  └──┘  └─────
par  ───────────┘             └─┘       └──┘  └──┘  └─────
pid  ───────────┘             └─┘       └──┘  └────┘       
st   ───────────────────────────────────────────────────────┘└───┘└───────
451      nonnegg_neg_pos.2 (sq_le_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))
id                          └──────────────────┘  └─────────────┘   └┘   └─────────────┘   └┘
src  ───┘               └─┘ └──────────────────┘ └─────────────┘└─┘  └┘ └─────────────┘└─┘  └──
typ  ───┘               └─┘ └──────────────────┘ └─────────────┘└─┘└┘└┘ └─────────────┘└─┘└┘└──
doc  ───┘               └─┘                                     └─┘  └┘                └─┘  └──
txt  ───┘               └─┘                                     └─┘  └┘                └─┘  └──
par  ───┘               └─┘                                     └─┘  └┘                └─┘  └──
pid  ───┘               └─┘                                     └─┘  └┘                └─┘  └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────
452    | ._, ._, ⟨x, y, or.inr $ or.inl rfl⟩, ⟨z, w, or.inr $ or.inr rfl⟩, ha, hb :=
id                               └────┘                       └────┘ └─┘
src  ─┘                          └────┘                       └────┘ └─┘
typ  ─┘                          └────┘                       └────┘ └─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
453      by rw [calc (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id                                                        └─┘
src         └──┘       └┘  └┘    └┘ └──┘   └┘  └──────┘└─┘
typ         └──┘       └┘  └┘    └┘ └──┘   └┘  └──────┘└─┘
doc         └──┘       └┘  └┘    └┘ └──┘   └┘  └──────┘   
txt         └──┘       └┘  └┘    └┘ └──┘   └┘  └──────┘   
par         └──┘       └┘  └┘    └┘ └──┘   └┘  └──────┘   
pid           └┘       └┘  └┘    └┘ └──┘   └┘  └──────┘   
st         └──────────────────────────────────────────────────
454          ... = ⟨-(x * z + d * y * w), x * w + y * z⟩ : by simp]; exact
id                                                
src  ───────────┘             └─┘       └──┘  └──┘  └─────
typ  ───────────┘            └─┘   └──┘  └──┘  └─────
doc  ───────────┘             └─┘       └──┘  └──┘  └─────
txt  ───────────┘             └─┘       └──┘  └──┘  └─────
par  ───────────┘             └─┘       └──┘  └──┘  └─────
pid  ───────────┘             └─┘       └──┘  └────┘       
st   ───────────────────────────────────────────────────────┘└───┘└───────
455      nonnegg_neg_pos.2 (sq_le_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))
id                          └────────────────────────┘  └─────────────┘   └┘   └─────────────┘   └┘
src  ───┘               └─┘ └────────────────────────┘ └─────────────┘└─┘  └┘ └─────────────┘└─┘  └──
typ  ───┘               └─┘ └────────────────────────┘ └─────────────┘└─┘└┘└┘ └─────────────┘└─┘└┘└──
doc  ───┘               └─┘                                           └─┘  └┘                └─┘  └──
txt  ───┘               └─┘                                           └─┘  └┘                └─┘  └──
par  ───┘               └─┘                                           └─┘  └┘                └─┘  └──
pid  ───┘               └─┘                                           └─┘  └┘                └─┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
456    | ._, ._, ⟨x, y, or.inr $ or.inl rfl⟩, ⟨z, w, or.inr $ or.inl rfl⟩, ha, hb :=
id                                                   └────┘   └────┘ └─┘
src  ─┘                                              └────┘   └────┘ └─┘
typ  ─┘                                              └────┘   └────┘ └─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
457      by rw [calc (⟨x, -y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id                                                        └─┘
src         └──┘       └┘  └┘   └┘  └──┘   └┘  └──────┘└─┘
typ         └──┘       └┘  └┘   └┘  └──┘   └┘  └──────┘└─┘
doc         └──┘       └┘  └┘   └┘  └──┘   └┘  └──────┘   
txt         └──┘       └┘  └┘   └┘  └──┘   └┘  └──────┘   
par         └──┘       └┘  └┘   └┘  └──┘   └┘  └──────┘   
pid           └┘       └┘  └┘   └┘  └──┘   └┘  └──────┘   
st         └──────────────────────────────────────────────────
458          ... = ⟨x * z + d * y * w, -(x * w + y * z)⟩ : by simp]; exact
id                                               
src  ───────────┘           └┘         └───┘  └──┘  └─────
typ  ───────────┘          └┘     └───┘  └──┘  └─────
doc  ───────────┘           └┘         └───┘  └──┘  └─────
txt  ───────────┘           └┘         └───┘  └──┘  └─────
par  ───────────┘           └┘         └───┘  └──┘  └─────
pid  ───────────┘           └┘         └───┘  └────┘       
st   ───────────────────────────────────────────────────────┘└───┘└───────
459      nonnegg_pos_neg.2 (sq_le_mul.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
id                          └─────────────────────────┘                    └┘   └─────────────┘   └┘
src  ───┘               └─┘ └─────────────────────────┘                └─┘  └┘ └─────────────┘└─┘  └──
typ  ───┘               └─┘ └─────────────────────────┘                └─┘└┘└┘ └─────────────┘└─┘└┘└──
doc  ───┘               └─┘                                            └─┘  └┘                └─┘  └──
txt  ───┘               └─┘                                            └─┘  └┘                └─┘  └──
par  ───┘               └─┘                                            └─┘  └┘                └─┘  └──
pid  ───┘               └─┘                                            └─┘  └┘                └─┘  └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
460    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
461  
462    protected theorem mul_nonneg (a b : ℤ√d) : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
id                                         └┘                     
src                                        └┘                        
typ                                        └┘                     
doc                                        └┘
463    by repeat {rw ← nonneg_iff_zero_le}; exact nonneg_mul
id                     └────────────────┘         └────────┘
src       └──────┘└───┘└────────────────┘  └────┘└────────┘
typ       └──────┘└───┘└────────────────┘  └────┘└────────┘
doc       └──────┘└───┘                    └────┘          
txt       └──────┘└───┘                    └────┘          
par       └──────┘└───┘                    └────┘          
pid             └─────┘                                   
st       └──────────────────────────────┘└┘└─────────────────
464  
src  
typ  
doc  
txt  
par  
pid  
st   
465    theorem not_sq_le_succ (c d y) (h : 0 < c) : ¬sq_le (y + 1) c 0 d :=
id                                                └───┘          
src  ─┘                                            └───┘    
typ  ─┘                                           └───┘          
doc  ─┘                                              └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
466    not_le_of_gt $ mul_pos (mul_pos h $ nat.succ_pos _) $ nat.succ_pos _
id     └──────────┘   └─────┘  └─────┘    └──────────┘      └──────────┘
src    └──────────┘   └─────┘  └─────┘     └──────────┘      └──────────┘
typ    └──────────┘   └─────┘  └─────┘    └──────────┘      └──────────┘
467  
468    /-- A nonsquare is a natural number that is not equal to the square of an
469      integer. This is implemented as a typeclass because it's a necessary condition
470      for much of the Pell equation theory. -/
471    class nonsquare (x : ℕ) : Prop := (ns : ∀n : ℕ, x ≠ n*n)
id                                                    
src                                                      
typ                                                   
472  
473    parameter [dnsq : nonsquare d]
id                       └───────┘
src                      └───────┘
typ                      └───────┘
doc                      └───────┘
474    include dnsq
475  
476    theorem d_pos : 0 < d := lt_of_le_of_ne (nat.zero_le _) $ ne.symm $ (nonsquare.ns d 0)
id                            └────────────┘  └─────────┘      └─────┘    └──────────┘ 
src                            └────────────┘  └─────────┘      └─────┘    └──────────┘
typ                           └────────────┘  └─────────┘      └─────┘    └──────────┘ 
477  
478    theorem divides_sq_eq_zero {x y} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
id                                                             
src                                                                   
typ                                                            
479    let g := x.gcd y in or.elim g.eq_zero_or_pos
id             └──┘     └─────┘ └─────────────┘
src              └──┘      └─────┘  └─────────────┘
typ            └──┘     └─────┘ └─────────────┘
480      (λH, ⟨nat.eq_zero_of_gcd_eq_zero_left H, nat.eq_zero_of_gcd_eq_zero_right H⟩)
id            └─────────────────────────────┘   └──────────────────────────────┘ 
src            └─────────────────────────────┘    └──────────────────────────────┘
typ           └─────────────────────────────┘   └──────────────────────────────┘ 
481      (λgpos, false.elim $
id         └──┘  └────────┘
src              └────────┘
typ        └──┘  └────────┘
482        let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := nat.exists_coprime gpos in
id         └─┘                                           └────────────────┘ └──┘
src                                                          └────────────────┘
typ        └─┘                                           └────────────────┘ └──┘
483        begin
st         └─────
484          rw [hx, hy] at h,
id               └┘  └┘
src          └──┘  └┘  └────┘
typ          └──┘└┘└┘└┘└────┘
doc          └──┘  └┘  └────┘
txt          └──┘  └┘  └────┘
par          └──┘  └┘  └────┘
pid            └┘  └┘  └───┘
st   ─────────────┘└──┘└───┘└─
485          have : m * m = d * (n * n) := nat.eq_of_mul_eq_mul_left (mul_pos gpos gpos)
id                                    └───────────────────────┘  └─────┘      └──┘
src          └─────┘        └───┘└───────────────────────┘ └─────┘        └─
typ          └─────┘     └───┘└───────────────────────┘ └─────┘    └──┘└─
doc          └─────┘          └───┘                                         └─
txt          └─────┘          └───┘                                         └─
par          └─────┘          └───┘                                         └─
pid          └───┘└┘          └──┘                                         └─
st   ────────────────────────────────────────────────────────────────────────────────────
486            (by simpa [mul_comm, mul_left_comm] using h),
id                        └──────┘  └───────────┘        
src  ─────────┘   └─────┘└──────┘└┘└───────────┘└──────┘ 
typ  ─────────┘   └─────┘└──────┘└┘└───────────┘└──────┘
doc  ─────────┘   └─────┘        └┘             └──────┘ 
txt  ─────────┘   └─────┘        └┘             └──────┘ 
par  ─────────┘   └─────┘        └┘             └──────┘ 
pid  ─────────┘   └──────┘        └┘             └──────┘ 
st   ────────────┘└──────────────────────────────────────┘└─
487          have co2 := let co1 := co.mul_right co in co1.mul co1,
id                                  └──────────┘ └┘       └──┘
src          └──────────┘   └──────┘└──────────┘  └──┘   └──┘
typ          └──────────┘   └──────┘└──────────┘└┘└──┘   └──┘
doc          └──────────┘   └──────┘              └──┘       
txt          └──────────┘   └──────┘              └──┘       
par          └──────────┘   └──────┘              └──┘       
pid          └──────┘└─┘   └──────┘              └──┘       
st   ────────────────────────────────────────────────────────────┘└─
488          exact nonsquare.ns d m (nat.dvd_antisymm (by rw this; apply dvd_mul_right) $
id                 └──────────┘    └──────────────┘        └──┘        └───────────┘
src          └────┘└──────────┘   └──────────────┘   └─┘    └┘└────┘└───────────┘└┘ 
typ          └────┘└──────────┘ └──────────────┘   └─┘└──┘└──────┘└───────────┘└┘ 
doc          └────┘                                  └─┘    └┘└────┘             └┘ 
txt          └────┘                                  └─┘    └┘└────┘             └┘ 
par          └────┘                                  └─┘    └──────┘             └┘ 
pid                                                 └──┘    └──────┘             └┘ 
st   ───────────────────────────────────────────────────┘└───────────────────────────┘└───
489            co2.dvd_of_dvd_mul_right $ by simp [this])
id             └──────────────────────┘            └──┘
src  ─────────┘└──────────────────────┘   └────┘    └─
typ  ─────────┘└──────────────────────┘   └────┘└──┘└─
doc  ─────────┘                           └────┘    └─
txt  ─────────┘                           └────┘    └─
par  ─────────┘                           └────┘    └─
pid  ─────────┘                           └─────┘    └┘
st   ──────────────────────────────────────┘└──────────┘└─
490        end)
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└─┘
491  
492    theorem divides_sq_eq_zero_z {x y : ℤ} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
id                                                                  
src                                                                        
typ                                                                 
493    by rw [mul_assoc, ← int.nat_abs_mul_self, ← int.nat_abs_mul_self, ← int.coe_nat_mul, ← mul_assoc] at h;
id            └───────┘    └──────────────────┘    └──────────────────┘    └─────────────┘    └───────┘
src       └──┘└───────┘└──┘└──────────────────┘└──┘└──────────────────┘└──┘└─────────────┘└──┘└───────┘└────┘
typ       └──┘└───────┘└──┘└──────────────────┘└──┘└──────────────────┘└──┘└─────────────┘└──┘└───────┘└────┘
doc       └──┘         └──┘                    └──┘                    └──┘               └──┘         └────┘
txt       └──┘         └──┘                    └──┘                    └──┘               └──┘         └────┘
par       └──┘         └──┘                    └──┘                    └──┘               └──┘         └────┘
pid         └┘         └──┘                    └──┘                    └──┘               └──┘         └───┘
st       └────────────┘└──────────────────────┘└──────────────────────┘└─────────────────┘└───────────┘└──────
494    exact let ⟨h1, h2⟩ := divides_sq_eq_zero (int.coe_nat_inj h) in
id                └┘  └┘     └────────────────┘  └─────────────┘ 
src    └────┘      └┘  └───┘└────────────────┘ └─────────────┘ └────
typ    └────┘    └┘└┘└┘└───┘└────────────────┘ └─────────────┘└────
doc    └────┘      └┘  └───┘                                   └────
txt    └────┘      └┘  └───┘                                   └────
par    └────┘      └┘  └───┘                                   └────
pid               └┘  └───┘                                   └────
st   ──────────────────────────────────────────────────────────────────
495    ⟨int.eq_zero_of_nat_abs_eq_zero h1, int.eq_zero_of_nat_abs_eq_zero h2⟩
id                                         └────────────────────────────┘
src  ─┘                                 └┘└────────────────────────────┘  └─
typ  ─┘                                 └┘└────────────────────────────┘  └─
doc  ─┘                                 └┘                                └─
txt  ─┘                                 └┘                                └─
par  ─┘                                 └┘                                └─
pid  ─┘                                 └┘                                
st   ─────────────────────────────────────────────────────────────────────────
496  
src  
typ  
doc  
txt  
par  
pid  
st   
497    theorem not_divides_square (x y) : (x + 1) * (x + 1) ≠ d * (y + 1) * (y + 1) :=
id                                                                 
src  ─┘                                                                 
typ  ─┘                                                            
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
498    λe, by have t := (divides_sq_eq_zero e).left; contradiction
id                      └────────────────┘ 
src           └────────┘ └────────────────┘ └────┘  └─────────────
typ          └────────┘ └────────────────┘└────┘  └─────────────
doc           └────────┘                    └────┘  └─────────────
txt           └────────┘                    └────┘  └─────────────
par           └────────┘                    └────┘  └─────────────
pid           └────┘└─┘                    └───┘               
st           └─────────────────────────────────────────────────────
499  
src  
typ  
doc  
txt  
par  
pid  
st   
500    theorem nonneg_antisymm : Π {a : ℤ√d}, nonneg a → nonneg (-a) → a = 0
id                                     └┘   └────┘    └────┘       
src  ─┘                                 └┘    └────┘     └────┘         
typ  ─┘                                └┘   └────┘    └────┘       
doc  ─┘                                 └┘    └────┘     └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
501    | ⟨0,         0⟩         xy yx := rfl
id                                       └─┘
src                                      └─┘
typ                                      └─┘
502    | ⟨-[1+ x],   -[1+ y]⟩   xy yx := false.elim xy
id        └──┘      └──┘      └┘       └────────┘
src       └──┘      └──┘               └────────┘
typ       └──┘      └──┘      └┘       └────────┘
503    | ⟨(x+1:nat), (y+1:nat)⟩ xy yx := false.elim yx
id            └─┘       └─┘      └┘    └────────┘
src           └─┘       └─┘            └────────┘
typ           └─┘       └─┘      └┘    └────────┘
504    | ⟨-[1+ x],   0⟩         xy yx := absurd xy (not_sq_le_succ _ _ _ dec_trivial)
id        └──┘                 └┘       └────┘     └────────────┘       └─────────┘
src       └──┘                          └────┘     └────────────┘       └─────────┘
typ       └──┘                 └┘       └────┘     └────────────┘       └─────────┘
doc                                                                      └─────────┘
505    | ⟨(x+1:nat), 0⟩         xy yx := absurd yx (not_sq_le_succ _ _ _ dec_trivial)
id            └─┘                 └┘    └────┘     └────────────┘       └─────────┘
src           └─┘                       └────┘     └────────────┘       └─────────┘
typ           └─┘                 └┘    └────┘     └────────────┘       └─────────┘
doc                                                                      └─────────┘
506    | ⟨0,         -[1+ y]⟩   xy yx := absurd xy (not_sq_le_succ _ _ _ d_pos)
id                   └──┘      └┘       └────┘     └────────────┘       └───┘
src                  └──┘               └────┘     └────────────┘       └───┘
typ                  └──┘      └┘       └────┘     └────────────┘       └───┘
507    | ⟨0,         (y+1:nat)⟩ _  yx := absurd yx (not_sq_le_succ _ _ _ d_pos)
id                       └─┘      └┘    └────┘     └────────────┘       └───┘
src                      └─┘            └────┘     └────────────┘       └───┘
typ                      └─┘      └┘    └────┘     └────────────┘       └───┘
508    | ⟨(x+1:nat), -[1+ y]⟩   (xy : sq_le _ _ _ _) (yx : sq_le _ _ _ _) :=
id            └─┘   └──┘           └───┘               └───┘
src           └─┘   └──┘            └───┘                └───┘
typ           └─┘   └──┘           └───┘               └───┘
doc                                   └───┘                └───┘
509      let t := le_antisymm yx xy in by rw[one_mul] at t; exact absurd t (not_divides_square _ _)
id               └─────────┘                └─────┘              └────┘   └────────────────┘
src               └─────────┘             └─┘└─────┘└────┘  └────┘└────┘  └────────────────┘└─────
typ              └─────────┘             └─┘└─────┘└────┘  └────┘└────┘ └────────────────┘└─────
doc                                       └─┘       └────┘  └────┘                          └─────
txt                                       └─┘       └────┘  └────┘                          └─────
par                                       └─┘       └────┘  └────┘                          └─────
pid                                                └───┘                                 └───┘
st                                       └─────────┘└──────────────────────────────────────────────
510    | ⟨-[1+ x],   (y+1:nat)⟩ (xy : sq_le _ _ _ _) (yx : sq_le _ _ _ _) :=
id        └──┘          └─┘        └───┘               └───┘
src  ─┘   └──┘          └─┘         └───┘                └───┘
typ  ─┘   └──┘          └─┘        └───┘               └───┘
doc  ─┘                               └───┘                └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
511      let t := le_antisymm xy yx in by rw[one_mul] at t; exact absurd t (not_divides_square _ _)
id               └─────────┘                └─────┘              └────┘   └────────────────┘
src               └─────────┘             └─┘└─────┘└────┘  └────┘└────┘  └────────────────┘└─────
typ              └─────────┘             └─┘└─────┘└────┘  └────┘└────┘ └────────────────┘└─────
doc                                       └─┘       └────┘  └────┘                          └─────
txt                                       └─┘       └────┘  └────┘                          └─────
par                                       └─┘       └────┘  └────┘                          └─────
pid                                                └───┘                                 └───┘
st                                       └─────────┘└──────────────────────────────────────────────
512  
src  
typ  
doc  
txt  
par  
pid  
st   
513    theorem le_antisymm {a b : ℤ√d} (ab : a ≤ b) (ba : b ≤ a) : a = b :=
id                                └┘                          
src  ─┘                           └┘                               
typ  ─┘                           └┘                          
doc  ─┘                           └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
514    eq_of_sub_eq_zero $ nonneg_antisymm ba (by rw neg_sub; exact ab)
id     └───────────────┘   └─────────────┘ └┘        └─────┘        └┘
src    └───────────────┘   └─────────────┘        └─┘└─────┘  └────┘
typ    └───────────────┘   └─────────────┘ └┘     └─┘└─────┘  └────┘└┘
doc                                               └─┘         └────┘
txt                                               └─┘         └────┘
par                                               └─┘         └────┘
pid                                                               
st                                               └───────────────────┘
515  
516    instance : decidable_linear_order ℤ√d :=
id                └────────────────────┘ └┘
src               └────────────────────┘ └┘
typ               └────────────────────┘ └┘
doc                                      └┘
517    { le_antisymm     := @zsqrtd.le_antisymm,
id                           └────────────────┘
src                          └────────────────┘
typ                          └────────────────┘
518      le_total        := zsqrtd.le_total,
id                          └─────────────┘
src                         └─────────────┘
typ                         └─────────────┘
519      decidable_le    := zsqrtd.decidable_le,
id                          └─────────────────┘
src                         └─────────────────┘
typ                         └─────────────────┘
520      ..zsqrtd.preorder }
id         └─────────────┘
src        └─────────────┘
typ        └─────────────┘
521  
522    protected theorem eq_zero_or_eq_zero_of_mul_eq_zero : Π {a b : ℤ√d}, a * b = 0 → a = 0 ∨ b = 0
id                                                                   └┘                 
src                                                                  └┘                     
typ                                                                  └┘                 
doc                                                                   └┘
523    | ⟨x, y⟩ ⟨z, w⟩ h := by injection h with h1 h2; exact
id                                       
src                            └────────┘ └─────────┘  └─────
typ                            └────────┘└─────────┘  └─────
doc                            └────────┘ └─────────┘  └─────
txt                            └────────┘ └─────────┘  └─────
par                            └────────┘ └─────────┘  └─────
pid                                      └─────────┘       
st                            └──────────────────────────────
524      have h1 : x*z = -(d*y*w), from eq_neg_of_add_eq_zero h1,
id                                   └───────────────────┘ └┘
src  ───┘    └────┘        └──────┘└───────────────────┘  └─
typ  ───┘    └────┘        └──────┘└───────────────────┘└┘└─
doc  ───┘    └────┘           └──────┘                       └─
txt  ───┘    └────┘           └──────┘                       └─
par  ───┘    └────┘           └──────┘                       └─
pid  ───┘    └────┘           └──────┘                       └─
st   ─────────────────────────────────────────────────────────────
525      have h2 : x*w = -(y*z), from eq_neg_of_add_eq_zero h2,
id                                                          └┘
src  ───┘    └────┘         └──────┘                       └─
typ  ───┘    └────┘         └──────┘                     └┘└─
doc  ───┘    └────┘         └──────┘                       └─
txt  ───┘    └────┘         └──────┘                       └─
par  ───┘    └────┘         └──────┘                       └─
pid  ───┘    └────┘         └──────┘                       └─
st   ───────────────────────────────────────────────────────────
526      have fin : x*x = d*y*y → (⟨x, y⟩:ℤ√d) = 0, from
id                      
src  ───┘    └─────┘             └┘ └┘   └┘ └────────
typ  ───┘    └─────┘            └┘ └┘   └┘ └────────
doc  ───┘    └─────┘             └┘ └┘   └┘ └────────
txt  ───┘    └─────┘             └┘ └┘   └┘ └────────
par  ───┘    └─────┘             └┘ └┘   └┘ └────────
pid  ───┘    └─────┘             └┘ └┘   └┘ └────────
st   ────────────────────────────────────────────────────
527      λe, match x, y, divides_sq_eq_zero_z e with ._, ._, ⟨rfl, rfl⟩ := rfl end,
id                     └──────────────────┘                              └─┘
src  ───┘ └─┘      └┘ └┘└──────────────────┘ └────┘  └┘  └┘    └┘   └───┘└─┘└─────
typ  ───┘ └─┘     └┘└┘└──────────────────┘ └────┘  └┘  └┘    └┘   └───┘└─┘└─────
doc  ───┘ └─┘      └┘ └┘                     └────┘  └┘  └┘    └┘   └───┘   └─────
txt  ───┘ └─┘      └┘ └┘                     └────┘  └┘  └┘    └┘   └───┘   └─────
par  ───┘ └─┘      └┘ └┘                     └────┘  └┘  └┘    └┘   └───┘   └─────
pid  ───┘ └─┘      └┘ └┘                     └────┘  └┘  └┘    └┘   └───┘   └─────
st   ───────────────────────────────────────────────────────────────────────────────
528      if z0 : z = 0 then if w0 : w = 0 then
id       └┘                          
src  ───┘└┘└────┘  └──────┘  └────┘  └───────
typ  ───┘└┘└────┘ └──────┘  └────┘ └───────
doc  ───┘  └────┘  └──────┘  └────┘  └───────
txt  ───┘  └────┘  └──────┘  └────┘  └───────
par  ───┘  └────┘  └──────┘  └────┘  └───────
pid  ───┘  └────┘  └──────┘  └────┘  └───────
st   ──────────────────────────────────────────
529        or.inr (match z, w, z0, w0 with ._, ._, rfl, rfl := rfl end)
id         └────┘
src  ─────┘└────┘       └┘ └┘  └┘  └────┘  └┘  └┘   └┘   └──┘   └─────
typ  ─────┘└────┘       └┘ └┘  └┘  └────┘  └┘  └┘   └┘   └──┘   └─────
doc  ─────┘             └┘ └┘  └┘  └────┘  └┘  └┘   └┘   └──┘   └─────
txt  ─────┘             └┘ └┘  └┘  └────┘  └┘  └┘   └┘   └──┘   └─────
par  ─────┘             └┘ └┘  └┘  └────┘  └┘  └┘   └┘   └──┘   └─────
pid  ─────┘             └┘ └┘  └┘  └────┘  └┘  └┘   └┘   └──┘   └─────
st   ───────────────────────────────────────────────────────────────────
530      else
src  ─────────
typ  ─────────
doc  ─────────
txt  ─────────
par  ─────────
pid  ─────────
st   ─────────
531         or.inl $ fin $ eq_of_mul_eq_mul_right w0 $ calc
id                 
src  ──────┘                                       
typ  ──────┘                                       
doc  ──────┘                                        
txt  ──────┘                                        
par  ──────┘                                        
pid  ──────┘                                        
st   ───────────────────────────────────────────────────────
532           x * x * w = -y * (x * z) : by simp [h2, mul_assoc, mul_left_comm]
id                                                └┘  └───────┘  └───────────┘
src  ────────┘             └──┘  └────┘  └┘└───────┘└┘└───────────┘└─
typ  ────────┘             └──┘  └────┘└┘└┘└───────┘└┘└───────────┘└─
doc  ────────┘             └──┘  └────┘  └┘         └┘             └─
txt  ────────┘             └──┘  └────┘  └┘         └┘             └─
par  ────────┘             └──┘  └────┘  └┘         └┘             └─
pid  ────────┘             └──┘  └─────┘  └┘         └┘             └─
st   ─────────────────────────────────────┘└────────────────────────────────────
533                 ... = d * y * y * w : by simp [h1, mul_assoc, mul_left_comm]
id                                                 └┘  └───────┘  └───────────┘
src  ──────────────┘└──┘        └─┘  └────┘  └┘└───────┘└┘└───────────┘└─
typ  ──────────────┘└──┘        └─┘  └────┘└┘└┘└───────┘└┘└───────────┘└─
doc  ──────────────┘└──┘        └─┘  └────┘  └┘         └┘             └─
txt  ──────────────┘└──┘        └─┘  └────┘  └┘         └┘             └─
par  ──────────────┘└──┘        └─┘  └────┘  └┘         └┘             └─
pid  ──────────────────┘        └─┘  └─────┘  └┘         └┘             └─
st   ──────────────┘└──────────────────────┘└────────────────────────────────────
534      else
src  ───┘└────
typ  ───┘└────
doc  ───┘└────
txt  ───┘└────
par  ───┘└────
pid  ─────────
st   ───┘└────
535         or.inl $ fin $ eq_of_mul_eq_mul_right z0 $ calc
id          └────┘        └────────────────────┘
src  ──────┘└────┘     └────────────────────┘       
typ  ──────┘└────┘    └────────────────────┘       
doc  ──────┘                                        
txt  ──────┘                                        
par  ──────┘                                        
pid  ──────┘                                        
st   ───────────────────────────────────────────────────────
536           x * x * z = d * -y * (x * w) : by simp [h1, mul_assoc, mul_left_comm]
id                                                   └┘  └───────┘  └───────────┘
src  ────────┘               └──┘  └────┘  └┘└───────┘└┘└───────────┘└─
typ  ────────┘              └──┘  └────┘└┘└┘└───────┘└┘└───────────┘└─
doc  ────────┘               └──┘  └────┘  └┘         └┘             └─
txt  ────────┘               └──┘  └────┘  └┘         └┘             └─
par  ────────┘               └──┘  └────┘  └┘         └┘             └─
pid  ────────┘               └──┘  └─────┘  └┘         └┘             └─
st   ─────────────────────────────────────────┘└────────────────────────────────────
537                 ... = d * y * y * z : by simp [h2, mul_assoc, mul_left_comm]
id                                               └┘  └───────┘  └───────────┘
src  ──────────────┘└──┘        └─┘  └────┘  └┘└───────┘└┘└───────────┘└─
typ  ──────────────┘└──┘      └─┘  └────┘└┘└┘└───────┘└┘└───────────┘└─
doc  ──────────────┘└──┘        └─┘  └────┘  └┘         └┘             └─
txt  ──────────────┘└──┘        └─┘  └────┘  └┘         └┘             └─
par  ──────────────┘└──┘        └─┘  └────┘  └┘         └┘             └─
pid  ──────────────────┘        └─┘  └─────┘  └┘         └┘             └─
st   ──────────────┘└──────────────────────┘└────────────────────────────────────
538  
src  
typ  
doc  
txt  
par  
pid  
st   
539    instance : integral_domain ℤ√d :=
id                └─────────────┘ └┘
src  ─┘           └─────────────┘ └┘
typ  ─┘           └─────────────┘ └┘
doc  ─┘                           └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
540    { zero_ne_one := zero_ne_one,
id                      └─────────┘
src                     └─────────┘
typ                     └─────────┘
541      eq_zero_or_eq_zero_of_mul_eq_zero := @zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero,
id                                             └──────────────────────────────────────┘
src                                            └──────────────────────────────────────┘
typ                                            └──────────────────────────────────────┘
542      ..zsqrtd.comm_ring }
id         └──────────────┘
src        └──────────────┘
typ        └──────────────┘
543  
544    protected theorem mul_pos (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) : 0 < a * b := λab,
id                                      └┘                                    └┘
src                                     └┘                                  
typ                                     └┘                                    └┘
doc                                     └┘
545    or.elim (eq_zero_or_eq_zero_of_mul_eq_zero (le_antisymm ab (mul_nonneg _ _ (le_of_lt a0) (le_of_lt b0))))
id     └─────┘  └───────────────────────────────┘  └─────────┘ └┘  └────────┘      └──────┘ └┘   └──────┘ └┘
src    └─────┘  └───────────────────────────────┘  └─────────┘     └────────┘      └──────┘      └──────┘
typ    └─────┘  └───────────────────────────────┘  └─────────┘ └┘  └────────┘      └──────┘ └┘   └──────┘ └┘
546      (λe, ne_of_gt a0 e)
id           └──────┘ └┘ 
src           └──────┘
typ          └──────┘ └┘ 
547      (λe, ne_of_gt b0 e)
id           └──────┘ └┘ 
src           └──────┘
typ          └──────┘ └┘ 
548  
549    instance : decidable_linear_ordered_comm_ring ℤ√d :=
id                └────────────────────────────────┘ └┘
src               └────────────────────────────────┘ └┘
typ               └────────────────────────────────┘ └┘
doc                                                  └┘
550    { add_le_add_left := @zsqrtd.add_le_add_left,
id                           └────────────────────┘
src                          └────────────────────┘
typ                          └────────────────────┘
551      add_lt_add_left := @zsqrtd.add_lt_add_left,
id                           └────────────────────┘
src                          └────────────────────┘
typ                          └────────────────────┘
552      zero_ne_one     := zero_ne_one,
id                          └─────────┘
src                         └─────────┘
typ                         └─────────┘
553      mul_nonneg      := @zsqrtd.mul_nonneg,
id                           └───────────────┘
src                          └───────────────┘
typ                          └───────────────┘
554      mul_pos         := @zsqrtd.mul_pos,
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
555      zero_lt_one     := dec_trivial,
id                          └─────────┘
src                         └─────────┘
typ                         └─────────┘
doc                         └─────────┘
556      ..zsqrtd.comm_ring, ..zsqrtd.decidable_linear_order }
id         └──────────────┘    └───────────────────────────┘
src        └──────────────┘    └───────────────────────────┘
typ        └──────────────┘    └───────────────────────────┘
557  
558    instance : decidable_linear_ordered_semiring ℤ√d := by apply_instance
id                └───────────────────────────────┘ └┘
src               └───────────────────────────────┘ └┘        └──────────────
typ               └───────────────────────────────┘ └┘       └──────────────
doc                                                 └┘        └──────────────
txt                                                           └──────────────
par                                                           └──────────────
pid                                                                         
st                                                           └───────────────
559    instance : linear_ordered_semiring ℤ√d           := by apply_instance
id                └─────────────────────┘ └┘
src  ─┘           └─────────────────────┘ └┘                  └──────────────
typ  ─┘           └─────────────────────┘ └┘                 └──────────────
doc  ─┘                                   └┘                  └──────────────
txt  ─┘                                                       └──────────────
par  ─┘                                                       └──────────────
pid  ─┘                                                                     
st   ─┘                                                      └───────────────
560    instance : ordered_semiring ℤ√d                  := by apply_instance
id                └──────────────┘ └┘
src  ─┘           └──────────────┘ └┘                         └──────────────
typ  ─┘           └──────────────┘ └┘                        └──────────────
doc  ─┘                            └┘                         └──────────────
txt  ─┘                                                       └──────────────
par  ─┘                                                       └──────────────
pid  ─┘                                                                     
st   ─┘                                                      └───────────────
561  
src  
typ  
doc  
txt  
par  
pid  
st   
562  end
563  end zsqrtd